feat: new ToExpr Name

`Quote Name` was already using the optimized `Syntax.mkNameLit`

src/Init/Meta.lean

@@ -950,28 +950,10 @@ private def getEscapedNameParts? (acc : List String) : Name → Option (List Str
     getEscapedNameParts? (s::acc) n
   | Name.num _ _ => none
 
-def quoteNameMk (n : Name) : Term :=
-  if isSimple n 0 then
-    mkStr n 0 #[]
-  else
-    go n
-where
-  isSimple (n : Name) (sz : Nat) : Bool :=
-    match n with
-    | .anonymous => 0 < sz && sz <= 8
-    | .str p _ => isSimple p (sz+1)
-    | _ => false
-
-  mkStr (n : Name) (sz : Nat) (args : Array Term) : Term :=
-    match n with
-    | .anonymous => Syntax.mkCApp (Name.mkStr3 "Lean" "Name" ("mkStr" ++ toString sz)) args.reverse
-    | .str p s => mkStr p (sz+1) (args.push (quote s))
-    | _ => unreachable!
-
-  go : Name → Term
-    | Name.anonymous => mkCIdent ``Name.anonymous
-    | Name.str n s => Syntax.mkCApp ``Name.mkStr #[go n, quote s]
-    | Name.num n i => Syntax.mkCApp ``Name.mkNum #[go n, quote i]
+def quoteNameMk : Name → Term
+  | .anonymous => mkCIdent ``Name.anonymous
+  | .str n s => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s]
+  | .num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i]
 
 instance : Quote Name `term where
   quote n := match getEscapedNameParts? [] n with

src/Lean/ToExpr.lean

@@ -44,10 +44,28 @@ instance : ToExpr Unit where
   toExpr     := fun _ => mkConst `Unit.unit
   toTypeExpr := mkConst ``Unit
 
-private def Name.toExprAux : Name → Expr
-  | .anonymous => mkConst ``Lean.Name.anonymous
-  | .str p s ..=> mkApp2 (mkConst ``Lean.Name.str) (toExprAux p) (toExpr s)
-  | .num p n ..=> mkApp2 (mkConst ``Lean.Name.num) (toExprAux p) (toExpr n)
+private def Name.toExprAux (n : Name) : Expr :=
+  if isSimple n 0 then
+    mkStr n 0 #[]
+  else
+    go n
+where
+  isSimple (n : Name) (sz : Nat) : Bool :=
+    match n with
+    | .anonymous => 0 < sz && sz <= 8
+    | .str p _ => isSimple p (sz+1)
+    | _ => false
+
+  mkStr (n : Name) (sz : Nat) (args : Array Expr) : Expr :=
+    match n with
+    | .anonymous => mkAppN (mkConst (.str ``Lean.Name ("mkStr" ++ toString sz))) args.reverse
+    | .str p s => mkStr p (sz+1) (args.push (toExpr s))
+    | _ => unreachable!
+
+  go : Name → Expr
+    | .anonymous => mkConst ``Lean.Name.anonymous
+    | .str p s ..=> mkApp2 (mkConst ``Lean.Name.str) (go p) (toExpr s)
+    | .num p n ..=> mkApp2 (mkConst ``Lean.Name.num) (go p) (toExpr n)
 
 instance : ToExpr Name where
   toExpr     := Name.toExprAux