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