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 = Nat.forM.loop n f n

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 = Nat.forRevM.loop f n

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 = Nat.foldM.loop f n n init

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 _fun_discr = pure _fun_discr
Nat.foldM.loop f n (Nat.succ i) _fun_discr = f (n - i - 1) _fun_discr >>= 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 = Nat.foldRevM.loop f n init

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 _fun_discr = pure _fun_discr
Nat.foldRevM.loop f (Nat.succ i) _fun_discr = f i _fun_discr >>= 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 = Nat.allM.loop n p n

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 = Nat.anyM.loop n p n

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