Set

Immutable set of elements, backed by a Python ``set``. Every operation returns a new set rather than mutating in place.

Imports

open Array;

Table of Contents

Types

(type)

Immutable set of elements, backed by a Python ``set``. Every operation returns a new set rather than mutating in place.

type Set a

Creates a new empty set.

def new : {s : (Set a) | size s = 0}

Adds an element, returning a new set (never smaller than the original).

def add (s : (Set a)) (x : a) : {s2 : (Set a) | size s2 ≥ size s}

Checks if the set contains an element at runtime.

def has (s : (Set a)) (x : a) : Bool

Removes an element, returning a new set. Removing an absent element is a no-op (unlike Python's ``set.remove``).

def remove (s : (Set a)) (x : a) : (Set a)

Returns the union of two sets.

def union (s1 : (Set a)) (s2 : (Set a)) : (Set a)

Returns the intersection of two sets.

def intersection (s1 : (Set a)) (s2 : (Set a)) : (Set a)

Returns the difference of two sets (elements in s1 but not in s2).

def difference (s1 : (Set a)) (s2 : (Set a)) : (Set a)

Returns the elements of the set as an array.

def toList (s : (Set a)) : (Array a)

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

uninterpreted

Number of elements, as an uninterpreted measure (no runtime value).

def size : (s : (Set a)) → Int

uninterpreted

Whether the set contains an element, as an uninterpreted predicate usable in refinements. Use ``has`` to test membership at runtime.

def contains : (s : (Set a)) → (x : a) → Bool