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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For