@[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
Instances For
@[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
Instances For
@[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
Instances For
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