theorem TLA.ProofMode.Entails_assumption {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (idx : Nat) (hlookup : (List.map NamedPred.pred hyps)[idx]? = some goal) : Entails hyps goal

def TLA.ProofMode.tlaAssumptionTac : Lean.ParserDescr

tla_assumption closes a proof-mode goal when the target predicate already appears among the temporal hypotheses.

For example, from a context containing hp : p,

tla_assumption

closes the goal p. The match is by definitional equality, so unfolded abbreviations of the same predicate are accepted.

Outside proof mode, tla_assumption falls back to Lean's ordinary assumption.

Equations

• TLA.ProofMode.tlaAssumptionTac = Lean.ParserDescr.node `TLA.ProofMode.tlaAssumptionTac 1024 (Lean.ParserDescr.nonReservedSymbol "tla_assumption" false)