def TLA.tacticTry_unfold_at_all_ : Lean.ParserDescr

Try to unfold the given identifiers everywhere.

Equations

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

def TLA.tacticTlaUnfold : Lean.ParserDescr

Unfold TLA definitions in all hypotheses and the goal.

Equations

• TLA.tacticTlaUnfold = Lean.ParserDescr.node `TLA.tacticTlaUnfold 1024 (Lean.ParserDescr.nonReservedSymbol "tlaUnfold" false)

def TLA.tacticTlaUnfold' : Lean.ParserDescr

Unfold TLA and execution definitions everywhere.

Equations

• TLA.tacticTlaUnfold' = Lean.ParserDescr.node `TLA.tacticTlaUnfold' 1024 (Lean.ParserDescr.nonReservedSymbol "tlaUnfold'" false)

def TLA.tacticTlaUnfoldSimp : Lean.ParserDescr

Unfold TLA definitions and simplify everywhere.

Equations

• TLA.tacticTlaUnfoldSimp = Lean.ParserDescr.node `TLA.tacticTlaUnfoldSimp 1024 (Lean.ParserDescr.nonReservedSymbol "tlaUnfoldSimp" false)

def TLA.tacticTlaUnfoldSimp' : Lean.ParserDescr

Unfold TLA and execution definitions and simplify everywhere.

Equations

• TLA.tacticTlaUnfoldSimp' = Lean.ParserDescr.node `TLA.tacticTlaUnfoldSimp' 1024 (Lean.ParserDescr.nonReservedSymbol "tlaUnfoldSimp'" false)

def TLA.tacticTlaNontemporalSimp : Lean.ParserDescr

Simplify with the non-temporal TLA lemmas everywhere.

Equations

• TLA.tacticTlaNontemporalSimp = Lean.ParserDescr.node `TLA.tacticTlaNontemporalSimp 1024 (Lean.ParserDescr.nonReservedSymbol "tlaNontemporalSimp" false)

def TLA.changePredImpliesToValid : Lean.Elab.Tactic.TacticM Unit

Normalize a sequent goal into a validity goal, by definitional equality.

Equations

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