Data.Bag

Definitions

record Bag : Type -> Type

  Bag ~ Multiset, a set where each element can appear multiple times
  Free *commutative* monoid on a set
  Equivalently, a list without order, i.e. quotiented out by permutations
  Using the list representation here, without enforcing permutation quotient

Totality: total
Visibility: public export
Constructor: 

MkBag : List a -> Bag a

Projection: 

.toList : Bag a -> List a

Hints:

Applicative Bag

Foldable Bag

Functor Bag

Monad Bag

.toList : Bag a -> List a

Totality: total
Visibility: public export

toList : Bag a -> List a

Totality: total
Visibility: public export

Multiset : Type -> Type

Totality: total
Visibility: public export

multiplicities : Eq a => List a -> a -> Nat

Totality: total
Visibility: public export

multiplicities : Eq a => Bag a -> a -> Nat

  A multiset is equivalently a function `a -> Nat` with finite support

Totality: total
Visibility: public export

(++) : Bag a -> Bag a -> Bag a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

All : (a -> Type) -> Bag a -> Type

Totality: total
Visibility: public export

Any : (a -> Type) -> Bag a -> Type

Totality: total
Visibility: public export