dfoldrM

theorem Fin.dfoldrM_loop_zero {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1) → Type u_1} {h : 0 < n + 1} [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α ⟨0, h⟩) : dfoldrM.loop n α f 0 h x = pure x

theorem Fin.dfoldrM_loop_succ {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1) → Type u_1} {i : Nat} {h : i + 1 < n + 1} [Monad m] (f : (i : Fin n) → α i.succ → m (α i.castSucc)) (x : α ⟨i + 1, h⟩) : dfoldrM.loop n α f (i + 1) h x = f ⟨i, ⋯⟩ x >>= dfoldrM.loop n α f i ⋯

theorem Fin.dfoldrM_loop {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} {i : Nat} {h : i + 1 < n + 1 + 1} [Monad m] [LawfulMonad m] (f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)) (x : α ⟨i + 1, h⟩) : dfoldrM.loop (n + 1) α f (i + 1) h x = dfoldrM.loop n (α ∘ succ) (fun (x : Fin n) => f x.succ) i ⋯ x >>= f 0

@[simp]

theorem Fin.dfoldrM_zero {m : Type u_1 → Type u_2} {α : Fin (0 + 1) → Type u_1} [Monad m] (f : (i : Fin 0) → α i.succ → m (α i.castSucc)) (x : α (last 0)) : dfoldrM 0 α f x = pure x

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

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

theorem Fin.dfoldr_eq_dfoldrM {n : Nat} {α : Fin (n + 1) → Type u_1} (f : (i : Fin n) → α i.succ → α i.castSucc) (x : α (last n)) : dfoldr n α f x = dfoldrM n α f x

dfoldr

@[simp]

theorem Fin.dfoldr_zero {α : Fin (0 + 1) → Type u_1} (f : (i : Fin 0) → α i.succ → α i.castSucc) (x : α (last 0)) : dfoldr 0 α f x = x

theorem Fin.dfoldr_succ {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (last (n + 1))) : dfoldr (n + 1) α f x = f 0 (dfoldr n (α ∘ succ) (fun (x : Fin n) => f x.succ) x)

theorem Fin.dfoldr_succ_last {n : Nat} {α : Fin (n + 2) → Type u_1} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (last (n + 1))) : dfoldr (n + 1) α f x = dfoldr n (α ∘ castSucc) (fun (x : Fin n) => f x.castSucc) (f (last n) x)

theorem Fin.dfoldr_eq_foldr {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : dfoldr n (fun (x : Fin (n + 1)) => α) f x = foldr n f x

dfoldlM

theorem Fin.dfoldlM_loop_lt {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1) → Type u_1} {i : Nat} [Monad m] (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (h : i < n) (x : α ⟨i, ⋯⟩) : dfoldlM.loop n α f i ⋯ x = f ⟨i, h⟩ x >>= dfoldlM.loop n α f (i + 1) ⋯

theorem Fin.dfoldlM_loop_eq {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1) → Type u_1} [Monad m] (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (x : α ⟨n, ⋯⟩) : dfoldlM.loop n α f n ⋯ x = pure x

@[simp]

theorem Fin.dfoldlM_zero {m : Type u_1 → Type u_2} {α : Fin (0 + 1) → Type u_1} [Monad m] (f : (i : Fin 0) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM 0 α f x = pure x

theorem Fin.dfoldlM_loop {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} {i : Nat} [Monad m] (f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)) (h : i < n + 1) (x : α ⟨i, ⋯⟩) : dfoldlM.loop (n + 1) α f i ⋯ x = do let x ← f ⟨i, h⟩ x dfoldlM.loop n (α ∘ succ) (fun (x1 : Fin n) (x2 : (α ∘ succ) x1.castSucc) => f x1.succ x2) i h x

theorem Fin.dfoldlM_succ {m : Type u_1 → Type u_2} {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} [Monad m] (f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)) (x : α 0) : dfoldlM (n + 1) α f x = do let x ← f 0 x dfoldlM n (α ∘ succ) (fun (x1 : Fin n) (x2 : (α ∘ succ) x1.castSucc) => f x1.succ x2) x

theorem Fin.dfoldlM_eq_foldlM {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] (f : Fin n → α → m α) (x : α) : dfoldlM n (fun (x : Fin (n + 1)) => α) f x = foldlM n (fun (x : α) (i : Fin n) => f i x) x

dfoldl

@[simp]

theorem Fin.dfoldl_zero {α : Fin (0 + 1) → Type u_1} (f : (i : Fin 0) → α i.castSucc → α i.succ) (x : α 0) : dfoldl 0 α f x = x

theorem Fin.dfoldl_succ {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0) : dfoldl (n + 1) α f x = dfoldl n (α ∘ succ) (fun (x1 : Fin n) (x2 : (α ∘ succ) x1.castSucc) => f x1.succ x2) (f 0 x)

theorem Fin.dfoldl_succ_last {n : Nat} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0) : dfoldl (n + 1) α f x = f (last n) (dfoldl n (α ∘ castSucc) (fun (x1 : Fin n) (x2 : (α ∘ castSucc) x1.castSucc) => f x1.castSucc x2) x)

theorem Fin.dfoldl_eq_dfoldlM {n : Nat} {α : Fin (n + 1) → Type u_1} (f : (i : Fin n) → α i.castSucc → α i.succ) (x : α 0) : dfoldl n α f x = dfoldlM n α f x

theorem Fin.dfoldl_eq_foldl {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : dfoldl n (fun (x : Fin (n + 1)) => α) f x = foldl n (fun (x : α) (i : Fin n) => f i x) x

Fin.fold{l/r}{M} equals List.fold{l/r}{M}

theorem Fin.foldl_eq_foldl_finRange {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : foldl n f x = List.foldl f x (List.finRange n)

theorem Fin.foldr_eq_foldr_finRange {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : foldr n f x = List.foldr f x (List.finRange n)