Bootstrapping definitions about arrays

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

def Array.zipWithIndex {α : Type u_1} (arr : Array α) : Array (α × Nat)

Turns #[a, b] into #[(a, 0), (b, 1)].

Equations

• Array.zipWithIndex arr = Array.mapIdx arr fun (i : Fin (Array.size arr)) (a : α) => (a, i.val)

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

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)

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

def Array.range (n : Nat) : Array Nat

The array #[0, 1, ..., n - 1].

Equations

• Array.range n = Nat.fold (flip Array.push) n #[]

def Array.flatten {α : Type u_1} (arr : Array (Array α)) : Array α

Turns #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯] into #[a₁, a₂, ⋯, b₁, b₂, ⋯]

Equations

• Array.flatten arr = Array.foldl (fun (acc a : Array α) => Array.append acc a) #[] arr 0 (Array.size arr)