mathlib documentation

core.init.control.combinators

def list.mmap {m : Type uType v} [monad m] {α : Type w} {β : Type u} :
(α → m β)list αm (list β)

Equations
def list.mmap' {m : Type → Type v} [monad m] {α : Type u} {β : Type} :
(α → m β)list αm unit

Equations
def mjoin {m : Type uType u} [monad m] {α : Type u} :
m (m α)m α

Equations
def list.mfilter {m : Type → Type v} [monad m] {α : Type} :
(α → m bool)list αm (list α)

Equations
def list.mfoldl {m : Type uType v} [monad m] {s : Type u} {α : Type w} :
(s → α → m s)s → list αm s

Equations
def list.mfoldr {m : Type uType v} [monad m] {s : Type u} {α : Type w} :
(α → s → m s)s → list αm s

Equations
def list.mfirst {m : Type uType v} [monad m] [alternative m] {α : Type w} {β : Type u} :
(α → m β)list αm β

Equations
def when {m : Type → Type} [monad m] (c : Prop) [h : decidable c] :
m unitm unit

Equations
def mcond {m : Type → Type} [monad m] {α : Type} :
m boolm αm αm α

Equations
def mwhen {m : Type → Type} [monad m] :
m boolm unitm unit

Equations
def monad.mapm {m : Type u_1Type u_2} [monad m] {α : Type u_3} {β : Type u_1} :
(α → m β)list αm (list β)

Equations
def monad.mapm' {m : Type → Type u_1} [monad m] {α : Type u_2} {β : Type} :
(α → m β)list αm unit

Equations
def monad.join {m : Type u_1Type u_1} [monad m] {α : Type u_1} :
m (m α)m α

Equations
def monad.filter {m : Type → Type u_1} [monad m] {α : Type} :
(α → m bool)list αm (list α)

Equations
def monad.foldl {m : Type u_1Type u_2} [monad m] {s : Type u_1} {α : Type u_3} :
(s → α → m s)s → list αm s

Equations
def monad.cond {m : Type → Type} [monad m] {α : Type} :
m boolm αm αm α

Equations
def monad.sequence {m : Type uType v} [monad m] {α : Type u} :
list (m α)m (list α)

Equations
def monad.sequence' {m : Type → Type u} [monad m] {α : Type} :
list (m α)m unit

Equations
def monad.whenb {m : Type → Type} [monad m] :
boolm unitm unit

Equations
def monad.unlessb {m : Type → Type} [monad m] :
boolm unitm unit

Equations