Functoriality of Multiset.

@[instance_reducible]

instance Multiset.functor : Functor Multiset

Equations

• Multiset.functor = { map := @Multiset.map }

@[simp]

theorem Multiset.fmap_def {α' β' : Type u_1} {s : Multiset α'} (f : α' → β') : f <$> s = map f s

instance Multiset.instLawfulFunctor : LawfulFunctor Multiset

def Multiset.traverse {F : Type u → Type u} [Applicative F] [CommApplicative F] {α' β' : 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

• Multiset.traverse f = Quotient.lift (Functor.map Multiset.ofList ∘ traverse f) ⋯

@[instance_reducible]

instance Multiset.instMonad : Monad Multiset

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Multiset.pure_def {α : Type u_1} : pure = singleton

@[simp]

theorem Multiset.bind_def {α β : Type u_1} : (fun (x1 : Multiset α) (x2 : α → Multiset β) => x1 >>= x2) = bind

instance Multiset.instLawfulMonad : LawfulMonad Multiset

@[simp]

theorem Multiset.map_comp_coe {α β : Type u_1} (h : α → β) : Functor.map h ∘ ofList = ofList ∘ Functor.map h

theorem Multiset.id_traverse {α : Type u_1} (x : Multiset α) : traverse pure x = pure x

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 α) : traverse h (map g x) = traverse (h ∘ g) x

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 α) : (fun {α : Type u_1} => eta.app α) (traverse f x) = traverse ((fun {α : Type u_1} => eta.app α) ∘ f) x