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

Posted in M1F, M40001, Type theory, undergrad maths | Tagged , | 8 Comments

Induction, and inductive types.

Induction in Lean isn’t just something which you do on natural numbers. Continue reading

Posted in Learning Lean, Type theory | Tagged , | 9 Comments