Additional definitions on ForInStep

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

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

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

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