theorem TLA.ProofMode.Entails_toggle_goal_under_always {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} : Entails (mapHypPreds always hyps) goal = Entails (mapHypPreds always hyps) [tlafml|□goal]

def TLA.ProofMode.tlaToggleGoalUnderAlwaysTac : Lean.ParserDescr

tla_toggle_goal_under_always toggles one leading □ on the current proof-mode goal when every temporal hypothesis has a leading □.

For example, with hp : □ p, it changes a proof-mode goal □ q to q:

tla_check_goal Entails [⟨"hp", [tlafml| □ p]⟩] [tlafml| □ q]
tla_toggle_goal_under_always
tla_check_goal Entails [⟨"hp", [tlafml| □ p]⟩] q

If the current goal has no leading □, the same tactic changes q to □ q:

tla_check_goal Entails [⟨"hp", [tlafml| □ p]⟩] q
tla_toggle_goal_under_always
tla_check_goal Entails [⟨"hp", [tlafml| □ p]⟩] [tlafml| □ q]

Equations

• TLA.ProofMode.tlaToggleGoalUnderAlwaysTac = Lean.ParserDescr.node `TLA.ProofMode.tlaToggleGoalUnderAlwaysTac 1024 (Lean.ParserDescr.nonReservedSymbol "tla_toggle_goal_under_always" false)