@[inline_if_reduce]

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

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

@[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.