@[inline]

def Nat.forM {m : Type → Type u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m 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

• n.forM f = Nat.forM.loop✝ n f n ⋯

@[inline]

def Nat.forRevM {m : Type → Type u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) : m 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

• n.forRevM f = Nat.forRevM.loop✝ n f n ⋯

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

• n.foldM f init = Nat.foldM.loop✝ n f n ⋯ init

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

• n.foldRevM f init = Nat.foldRevM.loop✝ n f n ⋯ init

@[inline]

def Nat.allM {m : Type → Type u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m 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

• n.allM p = Nat.allM.loop✝ n p n ⋯

@[inline]

def Nat.anyM {m : Type → Type u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) : m 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

• n.anyM p = Nat.anyM.loop✝ n p n ⋯