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

list.mmap f (h :: t) = f h >>= λ (h' : β), list.mmap f t >>= λ (t' : list β), return (h' :: t')
list.mmap f list.nil = return list.nil

@[simp]

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

list α → m unit

Equations

list.mmap' f (h :: t) = f h >> list.mmap' f t
list.mmap' f list.nil = return unit.star()

def mjoin {m : Type u → Type u} [monad m] {α : Type u} (a : m (m α)) :

m α

Equations

mjoin a = a >>= id

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

list α → m (list α)

Equations

list.mfilter f (h :: t) = f h >>= λ (b : bool), list.mfilter f t >>= λ (t' : list α), cond b (return (h :: t')) (return t')
list.mfilter f list.nil = return list.nil

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

(s → α → m s) → s → list α → m s

Equations

list.mfoldl f s_1 (h :: r) = f s_1 h >>= λ (s' : s), list.mfoldl f s' r
list.mfoldl f s_1 list.nil = return s_1

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

(α → s → m s) → s → list α → m s

Equations

list.mfoldr f s_1 (h :: r) = list.mfoldr f s_1 r >>= λ (s' : s), f h s'
list.mfoldr f s_1 list.nil = return s_1

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

list α → m β

Equations

list.mfirst f (a :: as) = (f a <|> list.mfirst f as)
list.mfirst f list.nil = failure

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

Equations

when c t = ite c t (has_pure.pure unit.star())

def mcond {m : Type → Type} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) :

m α

Equations

mcond mbool tm fm = mbool >>= λ (b : bool), cond b tm fm

def mwhen {m : Type → Type} [monad m] (c : m bool) (t : m unit) :

Equations

mwhen c t = mcond c t (return unit.star())

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

list α → m (list β)

Equations

monad.mapm = list.mmap

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

list α → m unit

Equations

monad.mapm' = list.mmap'

def monad.join {m : Type u_1 → Type u_1} [monad m] {α : Type u_1} (a : m (m α)) :

m α

Equations

monad.join = mjoin

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

list α → m (list α)

Equations

monad.filter = list.mfilter

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

monad.foldl = list.mfoldl

def monad.cond {m : Type → Type} [monad m] {α : Type} (mbool : m bool) (tm fm : m α) :

m α

Equations

monad.cond = mcond

def monad.sequence {m : Type u → Type v} [monad m] {α : Type u} :

list (m α) → m (list α)

Equations

monad.sequence (h :: t) = h >>= λ (h' : α), monad.sequence t >>= λ (t' : list α), return (h' :: t')
monad.sequence list.nil = return list.nil

def monad.sequence' {m : Type → Type u} [monad m] {α : Type} :

list (m α) → m unit

Equations

monad.sequence' (h :: t) = h >> monad.sequence' t
monad.sequence' list.nil = return unit.star()

def monad.whenb {m : Type → Type} [monad m] (b : bool) (t : m unit) :

Equations

monad.whenb b t = cond b t (return unit.star())

def monad.unlessb {m : Type → Type} [monad m] (b : bool) (t : m unit) :

Equations

monad.unlessb b t = cond b (return unit.star()) t