Next:
Martin-Löf's Inductive Equality
Up:
Providing logic and equality
Previous:
Logic
Equality
This section describes the directory
lib_equality
in which various definitions of equality are kept.
Martin-Löf's Inductive Equality
Leibniz Equality
Paulin-Mohring's Inductive Equality
Altenkirch-Streicher Elimination Rule
Theorems about Equality
Conor McBride
11/13/1998
