source
@[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)

Instances For

source
@[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)

Instances For