tla_start h₁ h₂ ... enters proof mode for a raw TLA sequent. It splits the
left-hand side conjunction into named temporal hypotheses and keeps the right
hand side as the proof-mode goal.
For example, from a raw goal (p ∧ q) |-tla- r,
tla_start hp hq
changes the proof state to a proof-mode context with hp : p, hq : q, and
goal r.
Equations
- One or more equations did not get rendered due to their size.