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.bind a f = match a with | ForInStep.done a => pure (ForInStep.done a) | ForInStep.yield a => f a

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

@[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.run x = match x with | ForInStep.done a => a | ForInStep.yield a => a

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