Init.Data.Nat.Control

source

@[inline]

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

m Unit

Equations

Nat.forM n f = (fun loop => loop n) (Nat.forM.loop n f)

source

@[specialize]

def Nat.forM.loop {m : Type → Type u_1} [inst : 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

source

@[inline]

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

m Unit

Equations

Nat.forRevM n f = (fun loop => loop n) (Nat.forRevM.loop f)

source

@[specialize]

def Nat.forRevM.loop {m : Type → Type u_1} [inst : 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

source

@[inline]

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

m α

Equations

Nat.foldM f init n = (fun loop => loop n init) (Nat.foldM.loop f n)

source

@[specialize]

def Nat.foldM.loop {α : Type u} {m : Type u → Type v} [inst : 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

source

@[inline]

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

m α

Equations

Nat.foldRevM f init n = (fun loop => loop n init) (Nat.foldRevM.loop f)

source

@[specialize]

def Nat.foldRevM.loop {α : Type u} {m : Type u → Type v} [inst : 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

source

@[inline]

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

m Bool

Equations

Nat.allM n p = (fun loop => loop n) (Nat.allM.loop n p)

source

@[specialize]

def Nat.allM.loop {m : Type → Type u_1} [inst : 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 a ← p (n - i - 1) match a with | true => Nat.allM.loop n p i | false => pure false

source

@[inline]

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

m Bool

Equations

Nat.anyM n p = (fun loop => loop n) (Nat.anyM.loop n p)

source

@[specialize]

def Nat.anyM.loop {m : Type → Type u_1} [inst : 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 a ← p (n - i - 1) match a with | true => pure true | false => Nat.anyM.loop n p i