mathlib documentation

core / init.control.combinators

@[simp]
def list.mmap {m : Type uType v} [monad m] {α : Type w} {β : Type u} (f : α → m β) :
list αm (list β)
Equations
Instances for list.mmap
@[simp]
def list.mmap' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → m β) :
list αm unit
Equations
Instances for list.mmap'
def mjoin {m : Type uType u} [monad m] {α : Type u} (a : m (m α)) :
m α
Equations
def list.mfilter {m : Type → Type v} [monad m] {α : Type} (f : α → 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} (f : α → m β) :
list αm β
Equations
def when {m : Type → Type} [monad m] (c : Prop) [h : decidable c] (t : m unit) :
Equations
def mcond {m : Type → Type} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) :
m α
Equations
def mwhen {m : Type → Type} [monad m] (c : m bool) (t : m unit) :
Equations
def monad.mapm {m : Type u_1Type u_2} [monad m] {α : Type u_3} {β : Type u_1} (f : α → m β) :
list αm (list β)
Equations
def monad.mapm' {m : Type → Type u_1} [monad m] {α : Type u_2} {β : Type} (f : α → m β) :
list αm unit
Equations
def monad.join {m : Type u_1Type u_1} [monad m] {α : Type u_1} (a : m (m α)) :
m α
Equations
def monad.filter {m : Type → Type u_1} [monad m] {α : Type} (f : α → 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} (mbool : m bool) (tm fm : 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] (b : bool) (t : m unit) :
Equations
def monad.unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) :
Equations