@[inline]
def List.scanlM {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (f : β → α → m β) (init : β) (l : List α) :
m (List β)
Folds a monadic function over a list from the left, accumulating partial results starting with
init. The accumulated values are combined with the each element of the list in order, using f.
Equations
- List.scanlM f init l = List.reverse <$> List.scanAuxM✝ f init l
Instances For
@[inline]
def List.scanrM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m β) (init : β) (xs : List α) :
m (List β)
Folds a monadic function over a list from the right, accumulating partial results starting with
init. The accumulated values are combined with the each element of the list in order, using f.
Equations
- List.scanrM f init xs = List.scanAuxM✝ (flip f) init xs.reverse
Instances For
@[inline]
Fold a function f over the list from the left, returning the list of partial results.
scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]
Equations
- List.scanl f init as = (List.scanlM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init as).run
Instances For
@[inline]
Fold a function f over the list from the right, returning the list of partial results.
scanr (+) 0 [1, 2, 3] = [6, 5, 3, 0]
Equations
- List.scanr f init as = (List.scanrM (fun (x1 : α) (x2 : β) => pure (f x1 x2)) init as).run