Documentation

Batteries.Control.ForInStep.Basic

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