mathlib3 documentation

core / init.control.combinators

@[simp]
def list.mmap {m : Type u Type v} [monad m] {α : Type w} {β : Type u} (f : α m β) :
list α m (list β)
Equations
Instances for list.mmap
def mjoin {m : Type u Type 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 u Type v} [monad m] {s : Type u} {α : Type w} :
(s α m s) s list α m s
Equations
def list.mfoldr {m : Type u Type v} [monad m] {s : Type u} {α : Type w} :
s m s) s list α m s
Equations
def list.mfirst {m : Type u Type 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_1 Type 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 β) :
Equations
def monad.join {m : Type u_1 Type 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_1 Type 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 u Type v} [monad m] {α : Type u} :
list (m α) m (list α)
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