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

Rename a hypothesis in a hypothesis list.

Equations

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

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 fun (x : NamedPred σ) => match x with | { name := name, pred := pred } => { name := newName, pred := pred }) goal = Entails hyps goal

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.