Bags

Bags are collections of elements of a single type. Other languages often call these collections "sets", but in Lean this word is quite overloaded.

This file defines two common classes of bag:

• [Bag]: no duplicates; math model is [Finset]
• [MultiBag]: duplicates; math model is [Multiset]

It also defines classes for read-only variants which do not include a way to insert or remove elements.

class LeanColls.Bag.ReadOnly (C : Type u) (τ : outParam (Type v)) extends Membership , LeanColls.ToMultiset , LeanColls.Fold , LeanColls.Size : Type (max (max u (u_1 + 1)) v)

[Bag] operations expected on read-only "set-like" collections.

Note that this requires ToMultiset even though the model is ToFinset; lawfulness is stated in terms of ToFinset, but some Bags can't provide ToFinset without some extra hypotheses.

class LeanColls.Bag (C : Type u) (τ : outParam (Type v)) extends LeanColls.Bag.ReadOnly , LeanColls.Insert : Type (max (max u (u_1 + 1)) v)

[Bag] includes operations expected on most "set-like" collections.

class LeanColls.MultiBag.ReadOnly (C : Type u) (τ : outParam (Type v)) extends Membership , LeanColls.ToMultiset , LeanColls.Fold , LeanColls.Size : Type (max (max u (u_1 + 1)) v)

[MultiBag] operations expected on read-only "multiset-like" collections

class LeanColls.MultiBag (C : Type u) (τ : outParam (Type v)) extends LeanColls.MultiBag.ReadOnly , LeanColls.Insert : Type (max (max u (u_1 + 1)) v)

[MultiBag] includes operations expected on most "multiset-like" collections