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