@[specialize #[]]

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

Combine all the values that can be represented by Fin n with an initial value, starting at 0 and nesting to the left.

Example:

• Fin.foldl 3 (· + ·.val) (0 : Nat) = ((0 + (0 : Fin 3).val) + (1 : Fin 3).val) + (2 : Fin 3).val

Equations

• Fin.foldl 0 x_3 x✝ = x✝
• Fin.foldl n.succ f x✝ = Fin.foldl n (fun (x : α) (i : Fin n) => f x i.succ) (f x✝ 0)

@[specialize #[]]

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.foldlTR {α : Sort u_1} (n : Nat) (f : α → Fin n → α) (init : α) : α

Tail-recursive implementation of Fin.foldl, used by the compiler.

Equations

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

@[inline]

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

Combine all the values that can be represented by Fin n with an initial value, starting at n - 1 and nesting to the right.

Example:

• Fin.foldr 3 (·.val + ·) (0 : Nat) = (0 : Fin 3).val + ((1 : Fin 3).val + ((2 : Fin 3).val + 0))

Equations

• Fin.foldr n f init = Fin.foldr.loop n f n ⋯ init

@[specialize #[]]

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 x_3 a = a
• Fin.foldr.loop n f i_1.succ h a = Fin.foldr.loop n f i_1 ⋯ (f ⟨i_1, h⟩ a)

@[inline]

def Fin.foldlM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : α → Fin n → m α) (init : α) : m α

Folds a monadic function over all the values in Fin n from left to right, starting with 0.

It is the sequence of steps:

Fin.foldlM n f x₀ = do
  let x₁ ← f x₀ 0
  let x₂ ← f x₁ 1
  ...
  let xₙ ← f xₙ₋₁ (n-1)
  pure xₙ

Equations

• Fin.foldlM n f init = Fin.foldlM.loop✝ n f init 0

@[inline]

def Fin.foldrM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (n : Nat) (f : Fin n → α → m α) (init : α) : m α

Folds a monadic function over Fin n from right to left, starting with n-1.

It is the sequence of steps:

Fin.foldrM n f xₙ = do
  let xₙ₋₁ ← f (n-1) xₙ
  let xₙ₋₂ ← f (n-2) xₙ₋₁
  ...
  let x₀ ← f 0 x₁
  pure x₀

Equations

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

foldlM

theorem Fin.foldlM_congr {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] {n k : Nat} (w : n = k) (f : α → Fin n → m α) : foldlM n f = foldlM k fun (x : α) (i : Fin k) => f x (Fin.cast ⋯ i)

@[simp]

theorem Fin.foldlM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : α → Fin 0 → m α) : foldlM 0 f = pure

theorem Fin.foldlM_succ {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin (n + 1) → m α) : foldlM (n + 1) f = fun (x : α) => f x 0 >>= foldlM n fun (x : α) (j : Fin n) => f x j.succ

theorem Fin.foldlM_succ_last {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] [LawfulMonad m] (f : α → Fin (n + 1) → m α) : foldlM (n + 1) f = fun (x : α) => do let x ← foldlM n (fun (x : α) (j : Fin n) => f x j.castSucc) x f x (last n)

Variant of foldlM_succ that splits off Fin.last n rather than 0.

theorem Fin.foldlM_add {m : Type u_1 → Type u_2} {α : Type u_1} {n k : Nat} [Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α) : foldlM (n + k) f = fun (x : α) => foldlM n (fun (x : α) (i : Fin n) => f x (castLE ⋯ i)) x >>= foldlM k fun (x : α) (i : Fin k) => f x (natAdd n i)

foldrM

theorem Fin.foldrM_congr {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] {n k : Nat} (w : n = k) (f : Fin n → α → m α) : foldrM n f = foldrM k fun (i : Fin k) => f (Fin.cast ⋯ i)

@[simp]

theorem Fin.foldrM_zero {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : Fin 0 → α → m α) : foldrM 0 f = pure

theorem Fin.foldrM_succ {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) : foldrM (n + 1) f = fun (x : α) => foldrM n (fun (i : Fin n) => f i.succ) x >>= f 0

theorem Fin.foldrM_succ_last {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + 1) → α → m α) : foldrM (n + 1) f = fun (x : α) => f (last n) x >>= foldrM n fun (i : Fin n) => f i.castSucc

theorem Fin.foldrM_add {m : Type u_1 → Type u_2} {n k : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin (n + k) → α → m α) : foldrM (n + k) f = fun (x : α) => foldrM k (fun (i : Fin k) => f (natAdd n i)) x >>= foldrM n fun (i : Fin n) => f (castLE ⋯ i)

foldl

theorem Fin.foldl_congr {α : Sort u_1} {n k : Nat} (w : n = k) (f : α → Fin n → α) : foldl n f = foldl k fun (x : α) (i : Fin k) => f x (Fin.cast ⋯ i)

@[csimp]

theorem Fin.foldl_eq_foldlTR : @foldl = @foldlTR

@[simp]

theorem Fin.foldl_zero {α : Sort u_1} (f : α → Fin 0 → α) (x : α) : foldl 0 f x = x

theorem Fin.foldl_succ {α : Sort u_1} {n : Nat} (f : α → Fin (n + 1) → α) (x : α) : foldl (n + 1) f x = foldl n (fun (x : α) (i : Fin n) => f x i.succ) (f x 0)

theorem Fin.foldl_succ_last {α : Sort u_1} {n : Nat} (f : α → Fin (n + 1) → α) (x : α) : foldl (n + 1) f x = f (foldl n (fun (x1 : α) (x2 : Fin n) => f x1 x2.castSucc) x) (last n)

theorem Fin.foldl_add {α : Sort u_1} {n m : Nat} (f : α → Fin (n + m) → α) (x : α) : foldl (n + m) f x = foldl m (fun (x : α) (i : Fin m) => f x (natAdd n i)) (foldl n (fun (x : α) (i : Fin n) => f x (castLE ⋯ i)) x)

theorem Fin.foldl_eq_foldlM {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : foldl n f x = (foldlM n (fun (x1 : α) (x2 : Fin n) => pure (f x1 x2)) x).run

theorem Fin.foldlM_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [Monad m] [LawfulMonad m] {n : Nat} {f : α → Fin n → α} : foldlM n (fun (x : α) (i : Fin n) => pure (f x i)) x = pure (foldl n f x)

foldr

theorem Fin.foldr_congr {α : Sort u_1} {n k : Nat} (w : n = k) (f : Fin n → α → α) : foldr n f = foldr k fun (i : Fin k) => f (Fin.cast ⋯ i)

@[simp]

theorem Fin.foldr_zero {α : Sort u_1} (f : Fin 0 → α → α) (x : α) : foldr 0 f x = x

theorem Fin.foldr_succ {n : Nat} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : foldr (n + 1) f x = f 0 (foldr n (fun (i : Fin n) => f i.succ) x)

theorem Fin.foldr_succ_last {n : Nat} {α : Sort u_1} (f : Fin (n + 1) → α → α) (x : α) : foldr (n + 1) f x = foldr n (fun (x : Fin n) => f x.castSucc) (f (last n) x)

theorem Fin.foldr_add {n m : Nat} {α : Sort u_1} (f : Fin (n + m) → α → α) (x : α) : foldr (n + m) f x = foldr n (fun (i : Fin n) => f (castLE ⋯ i)) (foldr m (fun (i : Fin m) => f (natAdd n i)) x)

theorem Fin.foldr_eq_foldrM {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : foldr n f x = (foldrM n (fun (x1 : Fin n) (x2 : α) => pure (f x1 x2)) x).run

theorem Fin.foldl_rev {n : Nat} {α : Sort u_1} (f : Fin n → α → α) (x : α) : foldl n (fun (x : α) (i : Fin n) => f i.rev x) x = foldr n f x

theorem Fin.foldr_rev {α : Sort u_1} {n : Nat} (f : α → Fin n → α) (x : α) : foldr n (fun (i : Fin n) (x : α) => f x i.rev) x = foldl n f x

theorem Fin.foldrM_pure {m : Type u_1 → Type u_2} {α : Type u_1} {x : α} [Monad m] [LawfulMonad m] {n : Nat} {f : Fin n → α → α} : foldrM n (fun (i : Fin n) (x : α) => pure (f i x)) x = pure (foldr n f x)