Module tactics 

Tactics over the kernel’s own goals: a goal state of metavariables, outside the trusted base.

A goal is a metavariable with the hypotheses in scope and the type it must inhabit. A tactic assigns the focused goal a term that may mention new metavariables; those are the new goals, front first, as Lean’s tactic framework builds a proof. Nothing here is trusted: a tactic only builds terms, and GoalState::qed instantiates the statement’s proof, requires it closed, and has the kernel check it against the statement exactly as a term written by hand. A tactic that cannot do what it is asked leaves the state as it was.

Hypotheses are locals (Term::Var). A term handed to a tactic reads a global named like a hypothesis of the focused goal as that hypothesis (GoalState::read), the scoping a proof script expects.

Structs

Goal

One open goal as a reader sees it: the hypotheses in scope, outermost first, and the target, every solved metavariable substituted.

GoalState

A proof under construction: the statement, the metavariables standing for its unproved parts, and the goals still open.

ScriptError

A script’s failure: the step, by position and as written, and why; no step when the script ran to its end and the proof is not done.

Enums

TacticError

Why a tactic did nothing, or why there is no proof yet.

TacticStep

One step of a tactic script (by intro A x; exact (refl A x)).

Constants

SIMP_STEPS

How many rewrites one simp makes before it is refused as not terminating.