lean2/library/logic/logic.md

logic

Logical constructions and theorems, beyond what has already been declared in init.datatypes and init.logic.

The subfolder logic.axioms declares additional axioms. The command import logic does not import any axioms by default.

• connectives : the propositional connectives
• eq : additional theorems for equality and disequality
• cast : casts and heterogeneous equality
• quantifiers : existential and universal quantifiers
• identities : some useful identities
• instances : class instances for eq and iff
• subsingleton
• default

Subfolders:

• axioms : additional axioms
• examples