tla_exit is the inverse of tla_start: it leaves the proof mode by
converting an Entails-shaped goal back into a raw |-tla- sequent whose
left-hand side is the conjunction of the proof-mode hypotheses.
For example, in a proof-mode context with hp : p, hq : q, and goal r,
tla_exit
changes the proof state back to (p ∧ q) |-tla- r. A single hypothesis
hp : p becomes p |-tla- r. An empty proof-mode context becomes the
canonical |-tla- r (i.e. valid r), rather than the equivalent
(⊤) |-tla- r.
Equations
- TLA.ProofMode.tlaExitTac = Lean.ParserDescr.node `TLA.ProofMode.tlaExitTac 1024 (Lean.ParserDescr.nonReservedSymbol "tla_exit" false)