@[inline]

def Fin.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

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

@[irreducible]

def Fin.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

• Fin.foldl.loop n f x i = if h : i < n then Fin.foldl.loop n f (f x ⟨i, h⟩) (i + 1) else x

@[inline]

def Fin.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

• Fin.foldr n f init = Fin.foldr.loop n f ⟨n, ⋯⟩ init

@[irreducible]

def Fin.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

• Fin.foldr.loop n f ⟨0, property⟩ x = x
• Fin.foldr.loop n f ⟨i.succ, h⟩ x = Fin.foldr.loop n f ⟨i, ⋯⟩ (f ⟨i, h⟩ x)