dfoldrM #
dfoldr #
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, ⋯⟩)
:
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
dfoldl #
Fin.fold{l/r}{M}
equals List.fold{l/r}{M}
#
@[deprecated Fin.foldlM_eq_foldlM_finRange (since := "2024-11-19")]
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 : α)
:
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 : α)
:
@[deprecated Fin.foldrM_eq_foldrM_finRange (since := "2024-11-19")]
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 : α)
:
Alias of Fin.foldrM_eq_foldrM_finRange
.
@[deprecated Fin.foldl_eq_foldl_finRange (since := "2024-11-19")]
Alias of Fin.foldl_eq_foldl_finRange
.
@[deprecated Fin.foldr_eq_foldr_finRange (since := "2024-11-19")]
Alias of Fin.foldr_eq_foldr_finRange
.