dfoldrM #
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⟩)
:
Fin.dfoldrM.loop (n + 1) α f (i + 1) h x = Fin.dfoldrM.loop n (α ∘ Fin.succ) (fun (x : Fin n) => f x.succ) i ⋯ 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 : (fun (x : Fin (n + 1)) => α) (Fin.last n))
:
Fin.dfoldrM n (fun (x : Fin (n + 1)) => α) f x = Fin.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 : α (Fin.last n))
:
Fin.dfoldr n α f x = Fin.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 : α (Fin.last 0))
:
Fin.dfoldr 0 α f x = x
dfoldlM #
@[irreducible]
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, ⋯⟩)
:
Fin.dfoldlM.loop (n + 1) α f i ⋯ x = do
let x ← f ⟨i, h⟩ x
Fin.dfoldlM.loop n (α ∘ Fin.succ) (fun (x1 : Fin n) (x2 : (α ∘ Fin.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)
:
Fin.dfoldlM (n + 1) α f x = do
let x ← f 0 x
Fin.dfoldlM n (α ∘ Fin.succ) (fun (x1 : Fin n) (x2 : (α ∘ Fin.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 : α)
:
Fin.dfoldlM n (fun (x : Fin (n + 1)) => α) f x = Fin.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)
:
Fin.dfoldl 0 α f x = x
theorem
Fin.dfoldl_eq_dfoldlM
{n : Nat}
{α : Fin (n + 1) → Type u_1}
(f : (i : Fin n) → α i.castSucc → α i.succ)
(x : α 0)
:
Fin.dfoldl n α f x = Fin.dfoldlM n α f x
Fin.fold{l/r}{M} equals List.fold{l/r}{M} #
theorem
Fin.foldlM_eq_foldlM_finRange
{m : Type u_1 → Type u_2}
{α : Type u_1}
{n : Nat}
[Monad m]
(f : α → Fin n → m α)
(x : α)
:
Fin.foldlM n f x = List.foldlM f x (List.finRange n)
@[deprecated Fin.foldlM_eq_foldlM_finRange]
theorem
Fin.foldlM_eq_foldlM_list
{m : Type u_1 → Type u_2}
{α : Type u_1}
{n : Nat}
[Monad m]
(f : α → Fin n → m α)
(x : α)
:
Fin.foldlM n f x = List.foldlM f x (List.finRange n)
Alias of Fin.foldlM_eq_foldlM_finRange.
theorem
Fin.foldrM_eq_foldrM_finRange
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(f : Fin n → α → m α)
(x : α)
:
Fin.foldrM n f x = List.foldrM f x (List.finRange n)
@[deprecated Fin.foldrM_eq_foldrM_finRange]
theorem
Fin.foldrM_eq_foldrM_list
{m : Type u_1 → Type u_2}
{n : Nat}
{α : Type u_1}
[Monad m]
[LawfulMonad m]
(f : Fin n → α → m α)
(x : α)
:
Fin.foldrM n f x = List.foldrM f x (List.finRange n)
Alias of Fin.foldrM_eq_foldrM_finRange.
theorem
Fin.foldl_eq_foldl_finRange
{α : Type u_1}
{n : Nat}
(f : α → Fin n → α)
(x : α)
:
Fin.foldl n f x = List.foldl f x (List.finRange n)
@[deprecated Fin.foldl_eq_foldl_finRange]
theorem
Fin.foldl_eq_foldl_list
{α : Type u_1}
{n : Nat}
(f : α → Fin n → α)
(x : α)
:
Fin.foldl n f x = List.foldl f x (List.finRange n)
Alias of Fin.foldl_eq_foldl_finRange.
theorem
Fin.foldr_eq_foldr_finRange
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : α)
:
Fin.foldr n f x = List.foldr f x (List.finRange n)
@[deprecated Fin.foldr_eq_foldr_finRange]
theorem
Fin.foldr_eq_foldr_list
{n : Nat}
{α : Type u_1}
(f : Fin n → α → α)
(x : α)
:
Fin.foldr n f x = List.foldr f x (List.finRange n)
Alias of Fin.foldr_eq_foldr_finRange.