def
list.mfoldr
{m : Type u → Type v}
[monad m]
{s : Type u}
{α : Type w}
(a : α → s → m s)
(a_1 : s)
(a_2 : 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 β)
(a : list α) :
m β
Equations
- list.mfirst f (a :: as) = (f a <|> list.mfirst f as)
- list.mfirst f list.nil = failure
def
monad.mapm
{m : Type u_1 → Type u_2}
[monad m]
{α : Type u_3}
{β : Type u_1}
(f : α → m β)
(a : list α) :
m (list β)
Equations
def
monad.mapm'
{m : Type → Type u_1}
[monad m]
{α : Type u_2}
{β : Type}
(f : α → m β)
(a : list α) :
m unit
Equations
Equations
def
monad.filter
{m : Type → Type u_1}
[monad m]
{α : Type}
(f : α → m bool)
(a : list α) :
m (list α)
Equations
def
monad.foldl
{m : Type u_1 → Type u_2}
[monad m]
{s : Type u_1}
{α : Type u_3}
(a : s → α → m s)
(a_1 : s)
(a_2 : list α) :
m s
Equations
Equations
Equations
- monad.sequence (h :: t) = h >>= λ (h' : α), monad.sequence t >>= λ (t' : list α), return (h' :: t')
- monad.sequence list.nil = return list.nil
Equations
- monad.sequence' (h :: t) = h >> monad.sequence' t
- monad.sequence' list.nil = return ()