The element type this Z-set ranges over.

A Z-set: a finitely-supported elt -> int weight map, kept canonical (no zero-weight entries).

The empty Z-set (additive identity).

is_zero z is true iff z has no elements (equivalently, total weight everywhere is 0).

singleton e w is the Z-set mapping e to w (and zero if w = 0).

of_list pairs sums the weights of repeated elements; entries that sum to 0 are dropped.

to_list z returns the (element, nonzero-weight) pairs, ordered by the element ELEMENT.compare.

weight z e is the weight of e in z (0 if absent).

add a b is the pointwise sum of weights, dropping any that cancel to 0. Commutative, associative, with identity zero.

negate z flips the sign of every weight (the additive inverse: add z (negate z) = zero).

sub a b is add a (negate b).

scale n z multiplies every weight by n (zero when n = 0).

map f z applies f to each element, summing the weights of elements that collide onto the same image (and dropping any that cancel). A linear operator: map f (add a b) = add (map f a) (map f b).

filter p z keeps the entries whose element satisfies p, weights unchanged. A linear operator.

distinct z is the set-semantics projection: every element with weight > 0 is mapped to weight 1; elements with weight <= 0 are dropped. Idempotent.

support z is the list of elements with nonzero weight, ordered by ELEMENT.compare.

cardinality z is the number of distinct elements with nonzero weight.

total_weight z is the sum of all weights (may be negative).

iter f z applies f element weight to each entry, in element order.

fold f z acc folds f element weight over the entries, in element order.

Structural equality (canonical form makes this exact set/weight equality).

Pretty-print a Z-set as {e1: w1, e2: w2, …}.