# Functoriality of Multiset. #

instance Multiset.functor :
Equations
@[simp]
theorem Multiset.fmap_def {α' : Type u_1} {β' : Type u_1} {s : Multiset α'} (f : α'β') :
f <\$> s =
Equations
def Multiset.traverse {F : Type u → Type u} [] [] {α' : Type u} {β' : Type u} (f : α'F β') :
Multiset α'F (Multiset β')

Map each element of a Multiset to an action, evaluate these actions in order, and collect the results.

Equations
Instances For
Equations
@[simp]
theorem Multiset.pure_def {α : Type u_1} :
pure = singleton
@[simp]
theorem Multiset.bind_def {α : Type u_1} {β : Type u_1} :
(fun (x : ) (x_1 : α) => x >>= x_1) = Multiset.bind
Equations
@[simp]
theorem Multiset.lift_coe {α : Type u_1} {β : Type u_2} (x : List α) (f : List αβ) (h : ∀ (a b : List α), a bf a = f b) :
Quotient.lift f h x = f x
@[simp]
theorem Multiset.map_comp_coe {α : Type u_1} {β : Type u_1} (h : αβ) :
Coe.coe = Coe.coe
theorem Multiset.id_traverse {α : Type u_1} (x : ) :
theorem Multiset.comp_traverse {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [] [] [] [] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αG β) (h : βH γ) (x : ) :
Multiset.traverse (Functor.Comp.mk g) x =
theorem Multiset.map_traverse {G : Type u_1 → Type u_1} [] [] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αG β) (h : βγ) (x : ) :
theorem Multiset.traverse_map {G : Type u_1 → Type u_1} [] [] {α : Type u_1} {β : Type u_1} {γ : Type u_1} (g : αβ) (h : βG γ) (x : ) :
theorem Multiset.naturality {G : Type u_1 → Type u_1} {H : Type u_1 → Type u_1} [] [] [] [] (eta : ) {α : Type u_1} {β : Type u_1} (f : αG β) (x : ) :
(fun {α : Type u_1} => eta.app α) () = Multiset.traverse ((fun {α : Type u_1} => eta.app α) f) x