rerevert

This reverts commit e551a366a0.

src/Init/Core.lean

@@ -837,9 +837,6 @@ instance : Trans Iff Iff Iff where
 theorem Eq.comm {a b : α} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm
 theorem eq_comm {a b : α} : a = b ↔ b = a := Eq.comm
 
-theorem HEq.comm {a : α} {b : β} : HEq a b ↔ HEq b a := Iff.intro HEq.symm HEq.symm
-theorem heq_comm {a : α} {b : β} : HEq a b ↔ HEq b a := HEq.comm
-
 @[symm] theorem Iff.symm (h : a ↔ b) : b ↔ a := Iff.intro h.mpr h.mp
 theorem Iff.comm: (a ↔ b) ↔ (b ↔ a) := Iff.intro Iff.symm Iff.symm
 theorem iff_comm : (a ↔ b) ↔ (b ↔ a) := Iff.comm

src/Init/Data/Array/Basic.lean

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

src/Init/Data/Array/Lemmas.lean

@@ -57,7 +57,9 @@ open Array
 
 /-! ### Lemmas about `List.toArray`. -/
 
-@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
+@[simp] theorem toArray_size (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[simp] theorem toArrayAux_size {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
 
@@ -65,7 +67,6 @@ open Array
 
 @[deprecated toArray_toList (since := "2024-09-09")]
 abbrev toArray_data := @toArray_toList
-
 @[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
     a.toArray[i] = a[i]'(by simpa using h) := rfl
 

src/Init/NotationExtra.lean

@@ -154,10 +154,6 @@ 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/Init/Prelude.lean

@@ -754,10 +754,10 @@ infer the proof of `Nonempty α`.
 noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
   Classical.choice inferInstance
 
-instance {α : Sort u} {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
+instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
-instance Pi.instNonempty {α : Sort u} {β : α → Sort v} [(a : α) → Nonempty (β a)] :
+instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
     Nonempty ((a : α) → β a) :=
   Nonempty.intro fun _ => Classical.ofNonempty
 
@@ -767,7 +767,7 @@ instance : Inhabited (Sort u) where
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
   default := fun _ => default
 
-instance Pi.instInhabited {α : Sort u} {β : α → Sort v} [(a : α) → Inhabited (β a)] :
+instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
     Inhabited ((a : α) → β a) where
   default := fun _ => default
 
@@ -2570,9 +2570,7 @@ structure Array (α : Type u) where
   /--
   Converts a `List α` into an `Array α`.
 
-  You can also use the synonym `List.toArray` when dot notation is convenient.
-
-  At runtime, this constructor is implemented by `List.toArrayImpl` and is O(n) in the length of the
+  At runtime, this constructor is implemented by `List.toArray` and is O(n) in the length of the
   list.
   -/
   mk ::

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 ``Array.mk [u]) type) listLit
+  return mkApp (mkApp (mkConst ``List.toArray [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. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `List.toArray` 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
-  | Array.mk _ as => getListLitOf? as f
+  | List.toArray _ as => getListLitOf? as f
   | _ => return none
 
 /--
 Check if an expression is an array literal
-(i.e. `Array.mk` applied to a nested chain of `List.cons`, ending at a `List.nil`),
+(i.e. `List.toArray` 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' ``Array.mk 2 then
+  if e.isAppOfArity' ``List.toArray 2 then
     listLit? e.appArg!'
   else
     none