3 ms·
Lean isn't classical. Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.
by tlringer 6y ago
Lean isn't classical.
Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.