chore: use Array.mk instead of List.toArray

src/Init/Data/Array/Basic.lean

@@ -18,7 +18,7 @@ universe u v w
 syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
 
 macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+  | `(#[ $elems,* ]) => `(Array.mk [ $elems,* ])
 
 variable {α : Type u}
 

src/Init/NotationExtra.lean

@@ -154,6 +154,10 @@ end Lean
     | _          => throw ()
   | _ => throw ()
 
+@[app_unexpander Array.mk] def unexpandArrayMk : Lean.PrettyPrinter.Unexpander
+  | `($(_) [$xs,*]) => `(#[$xs,*])
+  | _               => throw ()
+
 @[app_unexpander List.toArray] def unexpandListToArray : Lean.PrettyPrinter.Unexpander
   | `($(_) [$xs,*]) => `(#[$xs,*])
   | _               => throw ()

src/Lean/Meta/AppBuilder.lean

@@ -502,7 +502,7 @@ def mkListLit (type : Expr) (xs : List Expr) : MetaM Expr := do
 def mkArrayLit (type : Expr) (xs : List Expr) : MetaM Expr := do
   let u ← getDecLevel type
   let listLit ← mkListLit type xs
-  return mkApp (mkApp (mkConst ``List.toArray [u]) type) listLit
+  return mkApp (mkApp (mkConst ``Array.mk [u]) type) listLit
 
 def mkNone (type : Expr) : MetaM Expr := do
   let u ← getDecLevel type

src/Lean/Meta/LitValues.lean

@@ -202,19 +202,19 @@ def getListLit? (e : Expr) : MetaM (Option (Array Expr)) := getListLitOf? e fun
 
 /--
 Check if an expression is an array literal
-(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
 where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
 and return the array of recognised values.
 -/
 def getArrayLitOf? (e : Expr) (f : Expr → MetaM (Option α)) : MetaM (Option (Array α)) := do
   let e ← instantiateMVars e.consumeMData
   match_expr e with
-  | List.toArray _ as => getListLitOf? as f
+  | Array.mk _ as => getListLitOf? as f
   | _ => return none
 
 /--
 Check if an expression is an array literal
-(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
 returning the array of `Expr` values.
 -/
 def getArrayLit? (e : Expr) : MetaM (Option (Array Expr)) := getArrayLitOf? e fun s => return some s

src/Lean/Util/Recognizers.lean

@@ -97,7 +97,7 @@ partial def listLit? (e : Expr) : Option (Expr × List Expr) :=
   loop e []
 
 def arrayLit? (e : Expr) : Option (Expr × List Expr) :=
-  if e.isAppOfArity' ``List.toArray 2 then
+  if e.isAppOfArity' ``Array.mk 2 then
     listLit? e.appArg!'
   else
     none