Proof checking
Proof term
A term whose type is the proposition it proves.
Definition
Proof term
Under the propositions-as-types interpretation, a proof term is a value accepted at the type representing a proposition.
The kernel infers or checks the term's type. If that type matches the theorem statement, the term proves the theorem under the calculus and environment.
01
Example
A function taking proofs of P and Q and returning the proof of P is a proof of P ∧ Q → P.
02
Important distinction
A tactic script is a program that may construct a proof term; it is not necessarily the object the kernel finally checks.
After reading this article, you should be able to
- Define Proof term in the sense used on this site.
- Read a small proof term as both a program and a proof.