@[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.done a_2).bind f = pure (ForInStep.done a_2)
- (ForInStep.yield a_2).bind f = f a_2

## Instances For

@[reducible, inline]

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 x.bind 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.done a_1).run = a_1
- (ForInStep.yield a_1).run = a_1

## 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 = x.bind fun (b : β) => do let x ← f a b ForInStep.bindList f l x