Documentation

Lean.Meta.Tactic.Rename

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

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

Equations
    Instances For