Proof checking
Definitional equality
Equality determined by the core computation rules rather than by a separate theorem.
Definition
Definitional equality
Two terms are definitionally equal when the kernel's reduction and unfolding rules identify them.
Definitional equality lets the type checker treat different surface forms as the same term. It is part of checking and needs no proof object at each use.
01
Example
The application (fun x => x) 3 is definitionally equal to 3.
02
Important distinction
Two mathematically equal expressions may not be definitionally equal and may require a theorem to relate them.
After reading this article, you should be able to
- Define Definitional equality in the sense used on this site.
- Distinguish computation-based equality from equality established by a theorem.