doc-next-gen

Init.Data.List.ToArrayImpl

Module docstring

{}

List.toArrayAux definition
: List α → Array α → Array α
Full source 
/--
Auxiliary definition for `List.toArray`.
`List.toArrayAux as r = r ++ as.toArray`
-/
@[inline_if_reduce]
def List.toArrayAux : List α → Array α → Array α
  | nil,       xs => xs
  | cons a as, xs => toArrayAux as (xs.push a)
List to Array Auxiliary Function
Informal description
The auxiliary function `List.toArrayAux` takes a list `as` of type `List α` and an array `r` of type `Array α`, and returns the concatenation of `r` with the array representation of `as`. Specifically, it processes the list recursively, appending each element of `as` to `r` in order.
List.toArrayImpl definition
(xs : List α) : Array α
Full source 
/--
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`.
-/
-- 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 (xs : List α) : Array α :=
  xs.toArrayAux (Array.mkEmpty xs.length)
List to array conversion implementation
Informal description
The function converts a list `xs` of type `List α` into an array of type `Array α` by initializing an empty array with capacity equal to the length of `xs` and then appending all elements of `xs` to it in order. The operation has time complexity $O(|xs|)$ where $|xs|$ is the length of the list.