Basic logical constants and checked definitions.
This module intentionally builds logic as environment declarations instead of
adding more trusted kernel terms. False, True, and, and their
eliminators/constructors are primitive constants for now; not is a checked
definition on top of the core calculus.
Summary
Functions
Returns a new environment extended with the initial logic library.
Extends an environment with the initial logical constants and definitions.
The proposition universe used by the initial logic library.