set
Totally ordered sets
type t<elt> = set<elt>
The type t<elt> is an alias for set<elt>.
let empty: <elt>t<elt>
The value empty denotes the empty set. In some contexts, it is
useful to annotate it with its type, for example:
(empty as set<int>).
let update: <elt>(_: elt) => (_: bool) => (_: t<elt>) => t<elt>
The call update(elt, true, set) is a copy of the set set
containing the element elt. The call update(elt, false, set) is a
copy of the set set where the element elt is absent.
let add: <elt>(_: elt) => (_: t<elt>) => t<elt>
The call add(elt, set) is a set containing all the elements of
the set set, plus the element elt.
let remove: <elt>(_: elt) => (_: t<elt>) => t<elt>
The call remove(elt, set) is a copy of the set set without the
element elt.
let literal: <elt>(_: list<elt>) => t<elt>
The call literal([e1, ..., en]) is a set containing
exactly the elements in the list. Note: The list must be literal,
not an expression (compile-time list of values).
let of_list: <elt>(_: list<elt>) => t<elt>
The call of_list(elements) is a set containing exactly the
elements in the list elements. Note: Use literal instead if
using a literal list. Note: Use literal instead if using a
literal list.
let size: <elt>(_: t<elt>) => nat
The call size(set) is the number of elements of the set set.
let cardinal: <elt>(_: t<elt>) => nat
The call cardinal(set) is the number of elements of the set set.
let mem: <elt>(_: elt) => (_: t<elt>) => bool
The call mem(elt, set) is true if, and only if, the element
elt belongs to the set set.
let fold: <elt, acc>(_: (_: [acc, elt]) => acc) => (_: t<elt>) => (_: acc) => acc
The call fold(f, set, init) is
f(... (f (f (init, e1), e2), ...), en),
where e1, e2, ..., en are the elements of the set set in
increasing order.
let fold_desc: <elt, acc>(_: (_: [elt, acc]) => acc) => (_: t<elt>) => (_: acc) => acc
The call fold(f, set, init) is f(... (f (init, en), ...), e1),
where e1, e2, ..., en are the elements of the set set in
increasing order.
let filter_map: <old, new>(_: (_: old) => option<new>) => (_: t<old>) => t<new>
The call filter_map(f, set) is a set made by calling f (the
filter) on each element of the set set: if f returns None(),
the element is skipped in the result, otherwise, if it is
Some(e), then e is kept.
let iter: <elt>(_: (_: elt) => unit) => (_: t<elt>) => unit
The call iter(f, set) applies f to all the elements of the set
set in increasing order.
let map: <old, new>(_: (_: old) => new) => (_: t<old>) => t<new>
The call map(f, set) evaluates in a set whose elements have been
obtained by applying f to the elements of the set set.