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 α).

@[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 α).

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

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.