tlaNormalize rewrites a raw TLA goal into a shape that proof-mode tactics can
introduce and split more predictably.
For example,
tlaNormalize
turns a valid implication goal such as |-tla- p → q into the corresponding
sequent shape p |-tla- q, and reassociates simple conjunction structure using
the proof-mode normalization simp set.
Equations
- TLA.ProofMode.tacticTlaNormalize = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaNormalize 1024 (Lean.ParserDescr.nonReservedSymbol "tlaNormalize" false)