Documentation

Std.Data.Array.Init.Basic

Bootstrapping definitions about arrays #

This file contains some definitions in Array needed for Std.List.Basic.

@[inline]
def Array.toListAppend {α : Type u_1} (as : Array α) (l : List α) :
List α

Like as.toList ++ l, but in a single pass.

Equations
def Array.ofFn {α : Type u_1} {n : Nat} (f : Fin nα) :

ofFn f with f : Fin n → α→ α returns the list whose ith element is f i.

ofFn f = #[f 0, f 1, ... , f(n - 1)]
Equations
def Array.ofFn.go {α : Type u_1} {n : Nat} (f : Fin nα) (i : Nat) (acc : Array α) :

Auxiliary for ofFn. ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]

Equations