def TLA.ProofMode.tacticTlaCheckGoalForm : Lean.ParserDescr

tlaCheckGoalForm checks that the current proof-mode goal is in the canonical literal Entails [...] goal form used by the proof-mode tactics.

It does not change the goal. This is useful in tests after a tactic that reflects over the hypothesis list: if the goal still contains unreduced list computations, then the check fails.

Equations

• TLA.ProofMode.tacticTlaCheckGoalForm = Lean.ParserDescr.node `TLA.ProofMode.tacticTlaCheckGoalForm 1024 (Lean.ParserDescr.nonReservedSymbol "tlaCheckGoalForm" false)

def TLA.ProofMode.tacticTla_check_goal_ : Lean.ParserDescr

tla_check_goal expected checks that the current proof-mode goal has the literal named hypothesis list and target predicate in expected.

Unlike show Entails [...] goal, this tactic does not forget proof-mode hypothesis names. For example,

tla_check_goal Entails [⟨"hp", p⟩, ⟨"hq", q⟩] r

checks that the context contains exactly hp : p followed by hq : q, and that the goal is r. Predicates are compared by definitional equality.

Equations

• One or more equations did not get rendered due to their size.