Set

Sets are unordered collections of unique values of the same type.

function empty : set('value)

Create an empty set.

const my_set : set (int) = Set.empty

Alternative syntax:

const my_set : set (int) = set []

function literal : list('value) -> set('value)

Create a non-empty set.

const my_set : set (int) = Set.literal (list [3; 2; 2; 1])

Or use the following syntax sugar:

const my_set : set (int) = set [3; 2; 2; 1]

function mem : 'value -> set('value) -> 'bool

Checks if a value exists in the set.

const contains_3 : bool = Set.mem(3, my_set)

Or:

const contains_3_alt : bool = my_set contains 3

function cardinal : set('value) -> nat

Number of elements in a set.

const cardinal : nat = Set.size (my_set)

Note that size is deprecated. Please use Set.size

function add : 'value -> set('value) -> set('value)

Add a value to a set.

function remove : 'value -> set('value) -> set('value)

Remove a value from a set.

function iter : ('a -> unit) -> set('a) -> unit

Iterate over values in a set.

function iter_op (const s : set (int)) : unit is

block {

function iterated (const i : int) : unit is

if i > 2 then Unit else (failwith ("Below range.") : unit)

} with Set.iter (iterated, s)

Note that set_iter is deprecated.

function fold : (('accumulator -> 'item -> 'accumulator) -> set ('item) -> 'accumulator) -> 'accumulator

Fold over values in a set

function sum (const acc : int; const i : int): int is acc + i

const sum_of_elements : int = Set.fold (sum, my_set, 0)

Note that set_fold is deprecated.