chore: use String.ofList instead of String.mk in elaborator+kernel

Author: TwoFX

src/Lean/Meta/ExprDefEq.lean

@@ -155,12 +155,12 @@ def isDefEqNat (s t : Expr) : MetaM LBool := do
     | none,   some t => isDefEq s t
     | none,   none   => pure LBool.undef
 
-/-- Support for constraints of the form `("..." =?= String.mk cs)` -/
+/-- Support for constraints of the form `("..." =?= String.ofList cs)` -/
 def isDefEqStringLit (s t : Expr) : MetaM LBool := do
   let isDefEq (s t) : MetaM LBool := toLBoolM <| Meta.isExprDefEqAux s t
-  if s.isStringLit && t.isAppOf ``String.mk then
+  if s.isStringLit && t.isAppOf ``String.ofList then
     isDefEq (← s.toCtorIfLit) t
-  else if s.isAppOf ``String.mk && t.isStringLit then
+  else if s.isAppOf ``String.ofList && t.isStringLit then
     isDefEq s (← t.toCtorIfLit)
   else
     pure LBool.undef

src/Lean/Meta/WHNF.lean

@@ -25,7 +25,7 @@ def toCtorIfLit : Expr → MetaM Expr
     if v == 0 then return mkConst ``Nat.zero
     else return mkApp (mkConst ``Nat.succ) (mkRawNatLit (v-1))
   | .lit (.strVal v) =>
-    Lean.Meta.whnf (mkApp (mkConst ``String.mk) (toExpr v.toList))
+    Lean.Meta.whnf (mkApp (mkConst ``String.ofList) (toExpr v.toList))
   | e => return e
 
 end Lean.Expr

src/kernel/inductive.cpp

@@ -1223,7 +1223,7 @@ void initialize_inductive() {
     mark_persistent(g_nat_zero->raw());
     g_nat_succ       = new expr(mk_constant(name{"Nat", "succ"}));
     mark_persistent(g_nat_succ->raw());
-    g_string_mk      = new expr(mk_constant(name{"String", "mk"}));
+    g_string_mk      = new expr(mk_constant(name{"String", "ofList"}));
     mark_persistent(g_string_mk->raw());
     expr char_type   = mk_constant(name{"Char"});
     g_list_cons_char = new expr(mk_app(mk_constant(name{"List", "cons"}, {level()}), char_type));

src/kernel/type_checker.cpp

@@ -1201,7 +1201,7 @@ void initialize_type_checker() {
     g_nat_xor      = new_persistent_expr_const({"Nat", "xor"});
     g_nat_shiftLeft  = new_persistent_expr_const({"Nat", "shiftLeft"});
     g_nat_shiftRight = new_persistent_expr_const({"Nat", "shiftRight"});
-    g_string_mk    = new_persistent_expr_const({"String", "mk"});
+    g_string_mk    = new_persistent_expr_const({"String", "ofList"});
     g_lean_reduce_bool = new_persistent_expr_const({"Lean", "reduceBool"});
     g_lean_reduce_nat  = new_persistent_expr_const({"Lean", "reduceNat"});
     register_name_generator_prefix(*g_kernel_fresh);