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

@[specialize #[]]

def Nat.forM.loop {m : Type → Type u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) (i : Nat) : i ≤ n → m Unit

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

@[specialize #[]]

def Nat.forRevM.loop {m : Type → Type u_1} [Monad m] (n : Nat) (f : (i : Nat) → i < n → m Unit) (i : Nat) : i ≤ n → m Unit

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

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

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

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

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

@[specialize #[]]

def Nat.allM.loop {m : Type → Type u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) (i : Nat) : i ≤ n → m Bool

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

@[specialize #[]]

def Nat.anyM.loop {m : Type → Type u_1} [Monad m] (n : Nat) (p : (i : Nat) → i < n → m Bool) (i : Nat) : i ≤ n → m Bool