# Additional definitions on `ForInStep` #

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

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

source
@[inline]
def ForInStep.run {α : Type u_1} :
ForInStep α → α

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

source
def ForInStep.bindList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) :
List α → ForInStep β → 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

Instances For