def TLA.ProofMode.tlaSimp : Lean.ParserDescr

tla_simp simplifies predicates in a proof-mode goal or selected proof-mode hypotheses, using Lean's simp arguments.

With no location, it simplifies the goal predicate. For example,

tla_simp [heq]

simplifies the goal using heq. With a location,

tla_simp [heq] at hp hq

simplifies only the temporal hypotheses hp and hq.

Equations

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

def TLA.ProofMode.tlaDsimp : Lean.ParserDescr

tla_dsimp definitionally simplifies predicates in a proof-mode goal or selected proof-mode hypotheses, using Lean's dsimp arguments.

For example, if hp has predicate wrap p and wrap unfolds to the identity, then

tla_dsimp [wrap] at hp

changes hp to have predicate p.

Equations

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