Next:
Leibniz Equality
Up:
Providing logic and equality
Previous:
Logic
Equality
This section describes the directory
lib_equality
in which various definitions of equality are kept.
Leibniz Equality
Paulin-Mohring's Inductive Equality
Martin-Löf's Inductive Equality
Altenkirch-Streicher Elimination Rule
Lego
Fri May 24 19:01:27 BST 1996