Proof checking
Elaborator
A program that turns convenient source syntax into explicit terms for a kernel.
Definition
Elaborator
An elaborator resolves omitted arguments, notation, overloaded names, and type information before kernel checking.
User-facing theorem statements are often shorter than the fully explicit core term. Elaboration produces the precise term and reports ambiguities or type errors.
01
Example
The source x + 0 relies on the elaborator to determine the type of x and which addition operation to use.
02
Important distinction
Kernel acceptance can keep an elaborator outside the trusted base when every generated term is checked again.
After reading this article, you should be able to
- Define Elaborator in the sense used on this site.
- Identify information an elaborator must add to a short source expression.