perf: remove List.redLength

src/Init/Data/Array/Basic.lean

@@ -11,6 +11,7 @@ import Init.Data.UInt.Basic
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
+import Init.Data.List.ToArray
 universe u v w
 
 /-! ### Array literal syntax -/

src/Init/Data/List.lean

@@ -23,3 +23,4 @@ import Init.Data.List.TakeDrop
 import Init.Data.List.Zip
 import Init.Data.List.Perm
 import Init.Data.List.Sort
+import Init.Data.List.ToArray

src/Init/Data/List/ToArray.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.List.Basic
+
+/--
+Auxiliary definition for `List.toArray`.
+`List.toArrayAux as r = r ++ as.toArray`
+-/
+@[inline_if_reduce]
+def List.toArrayAux : List α → Array α → Array α
+  | nil,       r => r
+  | cons a as, r => toArrayAux as (r.push a)
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
+def List.toArrayImpl (as : List α) : Array α :=
+  as.toArrayAux (Array.mkEmpty as.length)

src/Init/Prelude.lean

@@ -2716,28 +2716,6 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
--/
-@[inline_if_reduce]
-def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
-
-/-- A non-tail-recursive version of `List.length`, used for `List.toArray`. -/
-@[inline_if_reduce]
-def List.redLength : List α → Nat
-  | nil       => 0
-  | cons _ as => as.redLength.succ
-
-/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
--- This function is exported to C, where it is called by `Array.mk`
--- (the constructor) to implement this functionality.
-@[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArrayImpl (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.redLength)
-
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
 class Bind (m : Type u → Type v) where
   /-- If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the