Documentation

Lean.Meta.Tactic.Rename

source
def Lean.Meta.rename (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (newUserName : Lean.Name) :
Lean.MetaM Lean.MVarId
Equations
  • One or more equations did not get rendered due to their size.