4.1 KiB
4.1 KiB
id | title |
---|---|
set-reference | Set — Unordered unique collection of a type |
Defining a set
type int_set is set (int);
const my_set : int_set = set 1; 2; 3 end
type int_set = int set
let my_set : int_set =
Set.add 3 (Set.add 2 (Set.add 1 (Set.empty: int set)))
type int_set = set (int);
let my_set : int_set =
Set.add (3, Set.add (2, Set.add (1, Set.empty: set (int))));
Set.mem(is_member: a', s: a' set) : bool
Check if a set s
contains the element is_member
.
const contains_three : bool = my_set contains 3
// or alternatively
const contains_three_fn: bool = set_mem (3, my_set);
let contains_three: bool = Set.mem 3 my_set
let contains_three: bool = Set.mem(3, my_set);
Set.empty() : a' set
Create a new empty set. Needs to be annotated with the set type.
const my_set: int_set = set end
const my_set_2: int_set = set_empty
let my_set: int_set = (Set.empty: int set)
let my_set: int_set = (Set.empty: set (int));
Set.literal(element_list_literal: 'a list) : 'a set
Create a set from the elements of a list. Note that you must pass a list literal to this function, a variable will not work.
const s_fb : set(string) = set [
"foo" ;
"bar" ;
]
let literal_op (p: unit) : string set =
Set.literal ["foo"; "bar"; "foobar"]
let literal_op = (p: unit) : set(string) => Set.literal(["foo", "bar", "foobar"]);
Set.add(addition: a', s: a' set) : a' set
Add the element addition
to a set s
.
function add_op (const s : set(string)) : set(string) is
begin skip end with set_add("foobar" , s)
type int_set = int set
let my_set : int_set =
Set.add 3 (Set.add 2 (Set.add 1 (Set.empty: int set)))
type int_set = set (int);
let my_set : int_set =
Set.add (3, Set.add (2, Set.add (1, Set.empty: set (int))));
Set.remove(removal: a', s: a' set) : a' set
Remove the element removal
from a set s
.
const smaller_set: int_set = set_remove(3, my_set);
let smaller_set: int_set = Set.remove 3 my_set
let smaller_set: int_set = Set.remove(3, my_set);
Set.fold(folding_function: a' -> a' -> a', s: a' set, initial: a') : a'
Combine the elements of a set into a single value using a folding function.
function sum(const result: int; const i: int): int is result + i;
// Outputs 6
const sum_of_a_set: int = set_fold(sum, my_set, 0);
let sum (result, i: int * int) : int = result + i
let sum_of_a_set: int = Set.fold sum my_set 0
let sum = (result_i: (int, int)): int => result_i[0] + result_i[1];
let sum_of_a_set: int = Set.fold(sum, my_set, 0);
Set.size(s: a' set) : nat
Get the number of elements in a set.
const set_size: nat = size (my_set)
let set_size: nat = Set.size my_set
let set_size: nat = Set.size (my_set);