@[inline]

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

Equations

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

@[specialize #[]]

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

Equations

• Nat.forM.loop n f 0 = pure ()
• Nat.forM.loop n f (Nat.succ i) = 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 : Nat → m Unit) : m Unit

Equations

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

@[specialize #[]]

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

Equations

• Nat.forRevM.loop f 0 = pure ()
• Nat.forRevM.loop f (Nat.succ i) = do f i Nat.forRevM.loop f i

@[inline]

def Nat.foldM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α

Equations

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

@[specialize #[]]

def Nat.foldM.loop {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α

Equations

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

@[inline]

def Nat.foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (init : α) (n : Nat) : m α

Equations

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

@[specialize #[]]

def Nat.foldRevM.loop {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) : Nat → α → m α

Equations

• Nat.foldRevM.loop f 0 x = pure x
• Nat.foldRevM.loop f (Nat.succ i) x = f i x >>= Nat.foldRevM.loop f i

@[inline]

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

Equations

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

@[specialize #[]]

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

Equations

• Nat.allM.loop n p 0 = pure true
• Nat.allM.loop n p (Nat.succ i) = 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 : Nat → m Bool) : m Bool

Equations

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

@[specialize #[]]

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

Equations

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