Documentation

Init.Data.Nat.Control

@[inline]
def Nat.forM {m : TypeType u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < nm Unit) :

Executes a monadic action on all the numbers less than some bound, in increasing order.

Example:

#eval Nat.forM 5 fun i _ => IO.println i
0
1
2
3
4
Equations
    Instances For
      @[specialize #[]]
      def Nat.forM.loop {m : TypeType u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < nm Unit) (i : Nat) :
      i nm Unit
      Equations
        Instances For
          @[inline]
          def Nat.forRevM {m : TypeType u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < nm Unit) :

          Executes a monadic action on all the numbers less than some bound, in decreasing order.

          Example:

          #eval Nat.forRevM 5 fun i _ => IO.println i
          
          4
          3
          2
          1
          0
          
          Equations
            Instances For
              @[specialize #[]]
              def Nat.forRevM.loop {m : TypeType u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < nm Unit) (i : Nat) :
              i nm Unit
              Equations
                Instances For
                  @[inline]
                  def Nat.foldM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < nαm α) (init : α) :
                  m α

                  Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

                  Equations
                    Instances For
                      @[specialize #[]]
                      def Nat.foldM.loop {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < nαm α) (i : Nat) :
                      i nαm α
                      Equations
                        Instances For
                          @[inline]
                          def Nat.foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < nαm α) (init : α) :
                          m α

                          Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

                          Equations
                            Instances For
                              @[specialize #[]]
                              def Nat.foldRevM.loop {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat) (f : (i : Nat) → i < nαm α) (i : Nat) :
                              i nαm α
                              Equations
                                Instances For
                                  @[inline]
                                  def Nat.allM {m : TypeType u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < nm Bool) :

                                  Checks whether the monadic predicate p returns true for all numbers less that the given bound. Numbers are checked in increasing order until p returns false, after which no further are checked.

                                  Equations
                                    Instances For
                                      @[specialize #[]]
                                      def Nat.allM.loop {m : TypeType u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < nm Bool) (i : Nat) :
                                      i nm Bool
                                      Equations
                                        Instances For
                                          @[inline]
                                          def Nat.anyM {m : TypeType u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < nm Bool) :

                                          Checks whether there is some number less that the given bound for which the monadic predicate p returns true. Numbers are checked in increasing order until p returns true, after which no further are checked.

                                          Equations
                                            Instances For
                                              @[specialize #[]]
                                              def Nat.anyM.loop {m : TypeType u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < nm Bool) (i : Nat) :
                                              i nm Bool
                                              Equations
                                                Instances For