chore: don't use String->Name coercion, which may be removed (#11556)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Lean/Name.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import Std.Data.HashMap.Basic
 import Std.Lean.SMap
 import Std.Lean.Name
+import Lean.Meta.Match.MatcherInfo
 
 /-!
 # Additional functions on `Lean.Name`.

Mathlib/Tactic/ComputeDegree.lean

@@ -271,7 +271,7 @@ def getCongrLemma (twoH : Name × Name × List Bool) (debug : Bool := false) : N
       | true, true   => ``id
     | _ => ``id
   if debug then
-    let natr := if nam.getString == `trans then nam else nam.getString
+    let natr := if nam.getString == "trans" then nam.toString else nam.getString
     dbg_trace f!"congr lemma: '{natr}'"
     nam
   else

Mathlib/Tactic/DeriveTraversable.lean

@@ -85,7 +85,7 @@ This is convenient to make a definition with equation lemmas. -/
 def mkCasesOnMatch (type : Name) (levels : List Level) (params : List Expr) (motive : Expr)
     (indices : List Expr) (val : Expr)
     (rhss : (ctor : Name) → (fields : List FVarId) → TermElabM Expr) : TermElabM Expr := do
-  let matcherName ← getDeclName? >>= (fun n? => Lean.mkAuxName (n?.getD type ++ "match") 1)
+  let matcherName ← getDeclName? >>= (fun n? => Lean.mkAuxName (.mkStr (n?.getD type) "match") 1)
   let matchType ← generalizeTelescope (indices.concat val).toArray fun iargs =>
     mkForallFVars iargs (motive.beta iargs)
   let iinfo ← getConstInfoInduct type
@@ -158,8 +158,8 @@ def deriveFunctor (m : MVarId) : TermElabM Unit := do
   let d ← getConstInfo n
   let [m] ← run m <| evalTactic (← `(tactic| refine { map := @(?_) })) | failure
   let t ← m.getType >>= instantiateMVars
-  let n' := n ++ "map"
-  withDeclName n' <| withAuxDecl "map" t n' fun ad => do
+  let n' := .mkStr n "map"
+  withDeclName n' <| withAuxDecl (.mkSimple "map") t n' fun ad => do
     let m' := (← mkFreshExprSyntheticOpaqueMVar t).mvarId!
     mkMap n m'
     let e ← instantiateMVars (mkMVar m')
@@ -285,15 +285,15 @@ def deriveLawfulFunctor (m : MVarId) : TermElabM Unit := do
   xs.forM fun ⟨mim, _, _⟩ =>
     mim.withContext do
       if let (some (_, mim), _) ←
-          simpGoal mim (← rules [(``Functor.map_id, false)] [n ++ "map"] true) then
+          simpGoal mim (← rules [(``Functor.map_id, false)] [.mkStr n "map"] true) then
         mim.refl
   let (#[_, _, _, _, _, x], mcm) ← mcm.introN 6 | failure
   let (some mcm, _) ← dsimpGoal mcm (← rules [] [``Functor.map] false) | failure
   let xs ← mcm.induction x (mkRecName n)
   xs.forM fun ⟨mcm, _, _⟩ =>
     mcm.withContext do
       if let (some (_, mcm), _) ←
-          simpGoal mcm (← rules [(``Functor.map_comp_map, true)] [n ++ "map"] true) then
+          simpGoal mcm (← rules [(``Functor.map_comp_map, true)] [.mkStr n "map"] true) then
         mcm.refl
 
 /-- The deriving handler for `LawfulFunctor`. -/
@@ -399,8 +399,8 @@ def deriveTraversable (m : MVarId) : TermElabM Unit := do
   let d ← getConstInfo n
   let [m] ← run m <| evalTactic (← `(tactic| refine { traverse := @(?_) })) | failure
   let t ← m.getType >>= instantiateMVars
-  let n' := n ++ "traverse"
-  withDeclName n' <| withAuxDecl "traverse" t n' fun ad => do
+  let n' := .mkStr n "traverse"
+  withDeclName n' <| withAuxDecl (.mkSimple "traverse") t n' fun ad => do
     let m' := (← mkFreshExprSyntheticOpaqueMVar t).mvarId!
     mkTraverse n m'
     let e ← instantiateMVars (mkMVar m')
@@ -472,12 +472,12 @@ def deriveLawfulTraversable (m : MVarId) : TermElabM Unit := do
   let .app (.app (.const ``LawfulTraversable _) F) _ ← m.getType >>= instantiateMVars | failure
   let some n := F.getAppFn.constName? | failure
   let [mit, mct, mtmi, mn] ← m.applyConst ``LawfulTraversable.mk | failure
-  let defEqns : MetaM Simp.Context := rules [] [n ++ "map", n ++ "traverse"] true
+  let defEqns : MetaM Simp.Context := rules [] [.mkStr n "map", .mkStr n "traverse"] true
   traversableLawStarter mit n defEqns fun _ _ m => m.refl
   traversableLawStarter mct n defEqns fun _ _ m => do
-    if let (some (_, m), _) ←
-        simpFunctorGoal m (← rules [] [n ++ "map", n ++ "traverse", ``Function.comp] true) then
-    m.refl
+    if let (some (_, m), _) ← simpFunctorGoal m
+        (← rules [] [.mkStr n "map", .mkStr n "traverse", ``Function.comp] true) then
+      m.refl
   traversableLawStarter mtmi n defEqns fun _ _ m => do
     if let (some (_, m), _) ←
         simpGoal m (← rules [(``Traversable.traverse_eq_map_id', false)] [] false) then

Mathlib/Tactic/FunProp/ToStd.lean

@@ -109,7 +109,7 @@ def mkUncurryFun (n : Nat) (f : Expr) : MetaM Expr := do
       do return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes)
     let xProdType ← inferType (← mkProdElem xs)
 
-    withLocalDecl xProdName default xProdType λ xProd => do
+    withLocalDecl (.mkSimple xProdName) default xProdType λ xProd => do
       let xs' ← mkProdSplitElem xProd n
       mkLambdaFVars #[xProd] (← mkAppM' f xs').headBeta
 

Mathlib/Tactic/HelpCmd.lean

@@ -66,7 +66,7 @@ private def elabHelpOption (id : Option Ident) : CommandElabM Unit := do
     | .ofNat val => s!"Nat := {repr val}"
     | .ofInt val => s!"Int := {repr val}"
     | .ofSyntax val => s!"Syntax := {repr val}"
-    if let some val := opts.find name then
+    if let some val := opts.find (.mkSimple name) then
       msg1 := s!"{msg1}  (currently: {val})"
     msg := msg ++ .nest 2 (f!"option {name} : {msg1}" ++ .line ++ decl.descr) ++ .line ++ .line
   logInfo msg

Mathlib/Tactic/IntervalCases.lean

@@ -308,7 +308,7 @@ def intervalCases (g : MVarId) (e e' : Expr) (lbs ubs : Array Expr) (mustUseBoun
         let z := lo+i
         let rhs ← m.mkNumeral z
         let ty ← mkArrow (← mkEq e rhs) tgt
-        let goal ← mkFreshExprMVar ty .syntheticOpaque (appendTag tag (toString z))
+        let goal ← mkFreshExprMVar ty .syntheticOpaque (appendTag tag (.mkSimple (toString z)))
         goals := goals.push { rhs, value := z, goal := goal.mvarId! }
       m.bisect g goals.toSubarray z1 z2 e1 e2 p1 p2 e
       pure goals

Mathlib/Tactic/ProjectionNotation.lean

@@ -39,14 +39,14 @@ def mkExtendedFieldNotationUnexpander (f : Name) : CommandElabM Unit := do
       aux_def $(mkIdent <| Name.str f "unexpander") : Lean.PrettyPrinter.Unexpander := fun
         -- Having a zero-argument pattern prevents unnecessary parenthesization in output
         | `($$_ $$(x).$(mkIdent toA))
-        | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent projName))
+        | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent (.mkSimple projName)))
         | _ => throw ())
   else
     elabCommand <| ← `(command|
       @[app_unexpander $(mkIdent f)]
       aux_def $(mkIdent <| Name.str f "unexpander") : Lean.PrettyPrinter.Unexpander := fun
         -- Having this zero-argument pattern prevents unnecessary parenthesization in output
-        | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent projName))
+        | `($$_ $$x) => set_option hygiene false in `($$(x).$(mkIdent (.mkSimple projName)))
         | _ => throw ())
 
 /--

Mathlib/Tactic/TFAE.lean

@@ -165,7 +165,7 @@ def mkTFAEHypName (i j : TSyntax `num) (arr : TSyntax ``impArrow) : MetaM Name :
   | `(impArrow| → ) => pure "to"
   | `(impArrow| ↔ ) => pure "iff"
   | _ => throwErrorAt arr "expected '←', '→', or '↔'"
-  return String.intercalate "_" ["tfae", s!"{i.getNat}", arr, s!"{j.getNat}"]
+  return .mkSimple <| String.intercalate "_" ["tfae", s!"{i.getNat}", arr, s!"{j.getNat}"]
 
 open Elab in
 /-- The core of `tfae_have`, which behaves like `haveLetCore` in `Mathlib.Tactic.Have`. -/

Mathlib/Tactic/ToAdditive.lean

@@ -1086,7 +1086,8 @@ def proceedFields (src tgt : Name) : CoreM Unit := do
     else
       return #[]
   aux fun declName ↦ do match (← getEnv).find? declName with
-    | some (ConstantInfo.inductInfo {ctors := ctors, ..}) => return ctors.toArray.map (·.getString)
+    | some (ConstantInfo.inductInfo {ctors := ctors, ..}) =>
+        return ctors.toArray.map (.mkSimple ·.getString)
     | _ => pure #[]
 
 /-- Elaboration of the configuration options for `to_additive`. -/