Interface to stores
singleton el
(ix, store)
, where ix
is the index under which the only element el
was stored, and
store
is the store containing el
.add el s
(new_ix, new_store)
, where new_ix
is the index under which the new element el
was stored, and
new_store
is the new store containing el
.update ix el s
rebinds index ix
in store s
to point to
el
, and returns the resulting store. The previous binding
disappears. New indices resulting from further adds are guaranteed
to have higher indices.
ix
not bound.val iter : ('a ‑> unit) ‑> 'a t ‑> unit
iter f s
applies f
to all stored elements in store s
. The
order in which elements are passed to f
is unspecified.
iter f s
applies f
to all indexes and their related elements
in store s
. The order in which elements are passed to f
is
unspecified.
map f s
s
mapped from
their original value to the codomain of f
. Only the elements
are passed to f
. The order in which elements are passed to f
is unspecified.val fold : ('a ‑> 'b ‑> 'b) ‑> 'a t ‑> 'b ‑> 'b
fold f s a
computes (f eN ... (f e1 a) ...)
, where e1 ... eN
are the elements of all bindings in store s
. The order in which
the bindings are presented to f
is unspecified.
choose s
(ix, x)
, where ix
is the index
of some unspecified value x
in store s
.s
is empty.partition p s
(s1, s2)
, where
s1
is the store of all the elements of s
that satisfy the
predicate p
, and s2
is the store of all the elements of s
that do not satisfy p
.eq_classes eq s
(el, ec)
, where
el
is the only kind of element as identified by the equivalence
relation eq
stored in the equivalence class (store) ec
under
each index. Every such equivalence class is unique and maximal
with respect to s
, and the original indices of the elements are
preserved in each class.