Documentation

Lean.Meta.Tactic.Rename

source
def Lean.MVarId.rename (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (userNameNew : Lake.Name) :
Lean.MetaM Lean.MVarId

Rename the user-face naming for the free variable fvarId at mvarId.

Instances For
    source
    @[deprecated Lean.MVarId.rename]
    def Lean.Meta.rename (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newUserName : Lake.Name) :
    Lean.MetaM Lean.MVarId
    Instances For