def TLA.ProofMode.renameFun {σ : Type u} (newName : String) (h : NamedPred σ) : NamedPred σ

Change the displayed name of a hypothesis while retaining its predicate.

Equations

• TLA.ProofMode.renameFun newName h = { name := newName, pred := h.pred }

def TLA.ProofMode.renameHyp {σ : Type u} (hyps : List (NamedPred σ)) (oldName newName : String) : List (NamedPred σ)

Rename a hypothesis in a hypothesis list.

Equations

• TLA.ProofMode.renameHyp hyps oldName newName = TLA.ProofMode.modifyHypByName hyps oldName (TLA.ProofMode.renameFun newName)

theorem TLA.ProofMode.Entails_rename_by_name {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (newName oldName : String) : Entails (renameHyp hyps oldName newName) goal = Entails hyps goal

theorem TLA.ProofMode.Entails_rename_by_idx {σ : Type u} {hyps : List (NamedPred σ)} {goal : pred σ} (newName : String) (idx : Nat) : Entails (hyps.modify idx (renameFun newName)) goal = Entails hyps goal

def TLA.ProofMode.renameTacDSimps : Array Lean.Name

Reduction rules used after renaming a proof-mode hypothesis.

Equations

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

def TLA.ProofMode.tlaRename (old : TemporalHypLoc) (newStr : String) : Lean.Elab.Tactic.TacticM Unit

Rename the hypothesis at the given location.

def TLA.ProofMode.tlaRenameTac : Lean.ParserDescr

tla_rename h => h' renames a proof-mode temporal hypothesis. The predicate and the hypothesis position are unchanged.

For example, if the context contains hp : p, then

tla_rename hp => hp'

changes the context entry to hp' : p. A numeric index can be used instead of a name:

tla_rename 0 => hHead

Equations

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