Vortex.Journal.Marking

A multiset of tokens. The invariant, kept by every function here, is that no token is held with a count of zero, so two markings with the same tokens are equal as values.

The empty marking.

One token.

The marking holding each listed token once per mention.

The marking holding each token as many times as the counts say, summed over repeats.

Multiset sum: every token of both.

Multiset difference, truncated at zero. Where contains m n holds it is exact: plus (minus m n) n == m.

Inclusion: contains m n when m holds every token of n at least as often.

How many times a token is held.

Every token, repeated by its count, in token order.

Each token with its count, in token order.

The tokens held at least once.

The number of tokens, counted with multiplicity.

The tokens a predicate keeps, with their counts.

The monoid homomorphism a map on tokens extends to: each token is replaced by its image, counts multiplying. Markings are the free commutative monoid on tokens, so every homomorphism is one of these.

Do two markings share no token?