Equations
- Multiset.functor = { map := @Multiset.map, mapConst := fun {α β : Type ?u.8} => Multiset.map ∘ Function.const β }
def
Multiset.traverse
{F : Type u → Type u}
[Applicative F]
[CommApplicative F]
{α' β' : Type u}
(f : α' → F β')
:
Map each element of a Multiset
to an action, evaluate these actions in order,
and collect the results.
Equations
Instances For
@[simp]
theorem
Multiset.map_comp_coe
{α β : Type u_1}
(h : α → β)
:
Functor.map h ∘ ofList = ofList ∘ Functor.map h
theorem
Multiset.comp_traverse
{G H : Type u_1 → Type u_1}
[Applicative G]
[Applicative H]
[CommApplicative G]
[CommApplicative H]
{α β γ : Type u_1}
(g : α → G β)
(h : β → H γ)
(x : Multiset α)
:
traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) x = Functor.Comp.mk (traverse h <$> traverse g x)
theorem
Multiset.map_traverse
{G : Type u_1 → Type u_1}
[Applicative G]
[CommApplicative G]
{α β γ : Type u_1}
(g : α → G β)
(h : β → γ)
(x : Multiset α)
:
Functor.map h <$> traverse g x = traverse (Functor.map h ∘ g) x
theorem
Multiset.traverse_map
{G : Type u_1 → Type u_1}
[Applicative G]
[CommApplicative G]
{α β γ : Type u_1}
(g : α → β)
(h : β → G γ)
(x : Multiset α)
:
theorem
Multiset.naturality
{G H : Type u_1 → Type u_1}
[Applicative G]
[Applicative H]
[CommApplicative G]
[CommApplicative H]
(eta : ApplicativeTransformation G H)
{α β : Type u_1}
(f : α → G β)
(x : Multiset α)
: