Documentation

Lean.Meta.Tactic.Rename

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

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.rename mvarId fvarId newUserName = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `rename let a ← Lean.getLCtx let lctxNew : Lean.LocalContext := Lean.LocalContext.setUserName a fvarId newUserName let a ← Lean.Meta.getLocalInstances let a_1 ← Lean.Meta.getMVarType mvarId let a_2 ← Lean.Meta.getMVarTag mvarId let mvarNew ← Lean.Meta.mkFreshExprMVarAt lctxNew a a_1 Lean.MetavarKind.syntheticOpaque a_2 0 Lean.Meta.assignExprMVar mvarId mvarNew pure (Lean.Expr.mvarId! mvarNew)