Expand description
The Certifier: Converts DerivationTrees to Kernel Terms.
This is the Great Bridge between the Proof Engine and the Kernel. Via Curry-Howard, each proof rule maps to a term constructor:
| DerivationTree Rule | Kernel Term |
|---|---|
| Axiom / PremiseMatch | Term::Global(name) |
| ModusPonens [impl, arg] | Term::App(certify(impl), certify(arg)) |
| ConjunctionIntro [p, q] | conj P Q p_proof q_proof |
Structs§
- Certification
Context - Context for certifying derivation trees into kernel terms.
Functions§
- certify
- Certify a derivation tree, producing a kernel term.