Module M_ORSet

Observed-Remove set.

Supports add, remove, lookup and merge operations. See Mutable_types.RSet. Contains two separate instances of a regular Map, one for adding (add_s) and the other for removing (remove_s).

add el t adds (unique (), el) to add_s, where unique is the result of calling Random.bits. This may or may not be enough entropy for your use case.

remove el t adds all {(u, el) | ∃ u : (u, el) ∈ add_s} to remove_s

Both lookup and value operate on the set difference add_s \ remove_s.

merge a b calls merges add_s_a with add_s_b and the same for b