Documentation

Lean.Meta.Tactic.Rename

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

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

Instances For