Module proof 

Portable proof plans.

A source proof keeps its structure: which variable is split by induction or case analysis, and the names of fields and induction hypotheses. It also keeps its hints: definitions to unfold, lemmas and hypotheses to use, and whether arithmetic or computation closes a goal. Each target emits its own tactics from the plan and its kernel re-checks the result, so a proof is never copied as text into a language that cannot check it.

Mirrors js/src/translation/proof.js.

Structs

TheoremHead

The theorem a proof belongs to, with its binders already hoisted.

Enums

ProofName

What a name in a proof refers to.

Traits

ProofContext

The checker’s view of the program, as a proof sees it.

Functions

normalise_proof

Normalises a surface proof into a portable plan.

prop_functions

Functions, in first-use order, that a proposition mentions.