@[inline]
def
ForInStep.bind
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
(a : ForInStep α)
(f : α → m (ForInStep α))
:
m (ForInStep α)
This is similar to a monadic bind operator, except that the two type parameters have to be
the same, which prevents putting a monad instance on ForInStepT m α := m (ForInStep α).
Equations
- ForInStep.bind a f = match a with | ForInStep.done a => pure (ForInStep.done a) | ForInStep.yield a => f a
@[inline, reducible]
abbrev
ForInStep.bindM
{m : Type u_1 → Type u_2}
{α : Type u_1}
[Monad m]
(a : m (ForInStep α))
(f : α → m (ForInStep α))
:
m (ForInStep α)
This is similar to a monadic bind operator, except that the two type parameters have to be
the same, which prevents putting a monad instance on ForInStepT m α := m (ForInStep α).
Equations
- ForInStep.bindM a f = do let x ← a ForInStep.bind x f
@[inline]
Get the value out of a ForInStep.
This is usually done at the end of a forIn loop to scope the early exit to the loop body.
Equations
- ForInStep.run x = match x with | ForInStep.done a => a | ForInStep.yield a => a
def
ForInStep.bindList
{m : Type u_1 → Type u_2}
{α : Type u_3}
{β : Type u_1}
[Monad m]
(f : α → β → m (ForInStep β))
:
Applies function f to each element of a list to accumulate a ForInStep value.
Equations
- ForInStep.bindList f [] x = pure x
- ForInStep.bindList f (a :: l) x = ForInStep.bind x fun (b : β) => do let x ← f a b ForInStep.bindList f l x