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

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

Equations

• Nat.forM.loop n f 0 x_2 = pure ()
• Nat.forM.loop n f i.succ h = do f (n - i - 1) ⋯ Nat.forM.loop n f i ⋯

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

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

Equations

• Nat.forRevM.loop n f 0 x_2 = pure ()
• Nat.forRevM.loop n f i.succ h = do f i ⋯ Nat.forRevM.loop n f i ⋯

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

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

• Nat.foldM.loop n f 0 h x = pure x
• Nat.foldM.loop n f i.succ h x = f (n - i - 1) ⋯ x >>= Nat.foldM.loop n f i ⋯

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

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

• Nat.foldRevM.loop n f 0 h x = pure x
• Nat.foldRevM.loop n f i.succ h x = f i ⋯ x >>= Nat.foldRevM.loop n f i ⋯

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

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

Equations

• Nat.allM.loop n p 0 x_2 = pure true
• Nat.allM.loop n p i.succ h = do let __do_lift ← p (n - i - 1) ⋯ match __do_lift with | true => Nat.allM.loop n p i ⋯ | false => pure false

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

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

Equations

• Nat.anyM.loop n p 0 x_2 = pure false
• Nat.anyM.loop n p i.succ h = do let __do_lift ← p (n - i - 1) ⋯ match __do_lift with | true => pure true | false => Nat.anyM.loop n p i ⋯