@[inline]

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

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

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 α

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 α

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

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

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 ⋯