Bootstrapping definitions about arrays

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

ink

@[inline]

def Array.toListAppend {α : Type u_1} (as : Array α) (l : List α) : List α

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

Equations

• Array.toListAppend as l = Array.foldr List.cons l as (Array.size as)

ink

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

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

• Array.ofFn f = Array.ofFn.go f 0 (Array.mkEmpty n)

ink

def Array.ofFn.go {α : Type u_1} {n : Nat} (f : Fin n → α) (i : Nat) (acc : Array α) : Array α

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

Equations

• Array.ofFn.go f i acc = if h : i < n then Array.ofFn.go f (i + 1) (Array.push acc (f { val := i, isLt := h })) else acc