Set

Table of Contents

Types

(type)

type Set a

Creates a new empty set.

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

Adds an element to the set.

def add : (s : Set a) -> (x : a) -> {s2 : Set a | size s2 >= size s}

Checks if the set contains an element.

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

Removes an element from the set.

def remove : (s : Set a) -> (x : {el : a | contains s el}) -> 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.

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

Returns the list of elements in the set.

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

Returns the size (number of elements) of the set.

def size : (s : Set a) -> Int

uninterpreted

Returns whether the set contains an element.

def contains : (s : Set a) -> (x : a) -> Bool