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