@[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} (as : List α) : Array α

Convert a List α into an Array α. This is O(n) in the length of the list.

Equations

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