@[inline]

def foldl {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) : α

Folds over Fin n from the left: foldl 3 f x = f (f (f x 0) 1) 2.

Equations

• foldl n f init = foldl.loop n f init 0

def foldl.loop {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (x : α) (i : Nat) : α

Inner loop for Fin.foldl. Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)

Equations

• foldl.loop n f x i = if h : i < n then foldl.loop n f (f x { val := i, isLt := h }) (i + 1) else x

@[inline]

def foldr {α : Sort u_1} (n : Nat) (f : Fin n → α → α) (init : α) : α

Folds over Fin n from the right: foldr 3 f x = f 0 (f 1 (f 2 x)).

Equations

• foldr n f init = foldr.loop n f { val := n, property := ⋯ } init

def foldr.loop {α : Sort u_1} (n : Nat) (f : Fin n → α → α) : { i : Nat // i ≤ n } → α → α

Inner loop for Fin.foldr. Fin.foldr.loop n f i x = f 0 (f ... (f (i-1) x))

Equations

• foldr.loop n f { val := 0, property := property } x = x
• foldr.loop n f { val := Nat.succ i, property := h } x = foldr.loop n f { val := i, property := ⋯ } (f { val := i, isLt := h } x)