Tag Archives: induction
Induction on equality
In type theory, equality has a definition, and basic facts about it such as symmetry and transitivity can be proved from more fundamental principles. Continue reading
Induction, and inductive types.
Induction in Lean isn’t just something which you do on natural numbers. Continue reading
Xena 