_aux_Mathlib_Tactic_Rename___elabRules_Mathlib_Tactic_rename'_1

Lean4

@[tactic Mathlib.Tactic.rename']
public meta def _aux_Mathlib_Tactic_Rename___elabRules_Mathlib_Tactic_rename'_1 : Lean.Elab.Tactic.Tactic✝ := fun
  | `(tactic| rename' $[$as:term => $bs:ident],*) => do
    let ids ← getFVarIds as
    liftMetaTactic1 fun goal ↦ do
        let mut lctx ← getLCtx
        for fvar in ids, tgt in bs do
          lctx := lctx.setUserName fvar tgt.getId
        let mvarNew ←
          mkFreshExprMVarAt lctx (← getLocalInstances) (← goal.getType) MetavarKind.syntheticOpaque (← goal.getTag)
        goal.assign mvarNew
        pure mvarNew.mvarId!
    withMainContext do
        for fvar in ids, tgt in bs do
          Elab.Term.addTermInfo' tgt (mkFVar fvar)
  | _ => no_error_if_unused% throwUnsupportedSyntax✝

Похожие утверждения