@[inline_if_reduce]

def List.toArrayAux {α : Type u_1} : List α → Array α → Array α

Auxiliary definition for List.toArray. List.toArrayAux as r = r ++ as.toArray

Equations

• [].toArrayAux x✝ = x✝
• (a :: as).toArrayAux x✝ = as.toArrayAux (x✝.push a)

@[match_pattern, inline, export lean_list_to_array]

def List.toArrayImpl {α : Type u_1} (xs : List α) : Array α

Converts a List α into an Array α by repeatedly pushing elements from the list onto an empty array. O(|xs|).

Use List.toArray instead of calling this function directly. At runtime, this operation implements both List.toArray and Array.mk.

Equations

• List.toArrayImpl xs = xs.toArrayAux (Array.mkEmpty xs.length)