*This section discusses axiomatic data types supported by VerCors.*


Axiomatic data types are data types that are defined by a set of uninterpreted functions and axioms that define the behavior of these functions. This is in contrast to concrete data types which are defined by their implementation in a programming language such as Java or C++. Axiomatic datatypes are not to be confused with _algebraic_ datatypes.

In the sections below, we are going to go over all ADTs supported by VerCors, give the definition of each, and show examples of common operations defined on them. A reference table can be found at the end showing all the operations defined on the ADTs.

The axiomatizations used by VerCors and its back end Viper can be found [here](https://github.com/viperproject/silicon/tree/master/src/main/resources/dafny_axioms) (for sequences sets and bags) and [here](https://github.com/utwente-fmt/vercors/tree/dev/src/main/universal/res/adt) (for the other ADTs).

Finally, it is also possible to create custom ADTs, though with limited syntax support. This is discussed at the end of this section.

# Sequence 
Sequences are an ordered/enumerated collection also commonly referred to as lists. Sequences are finite and immutable (i.e. once created they cannot be altered).

There are two ways to construct a sequence: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the sequence to be explicitly defined. For example, `s1` is a sequence of integers initialized with the values 1, 2 and 3 and `s2` is an empty sequence of integers.

<!-- testBlock Pass -->
```pvl
seq<int> s1 = seq<int> { 1, 2, 3 };
seq<int> s2 = seq<int> { };
```

The implicit syntax is a shorter syntax. If the sequence is initialized with at least one value (using the implicit syntax), VerCors infers the type of the sequence. An empty sequence can be constructed by providing the type of the sequence. For example, `s3` is equivalent to `s1` and `s4` is equivalent to `s2`. Notice how there is no space between `[` and `t`, this is mandated by the VerCors grammar.

<!-- testBlock Pass -->
```pvl
seq<int> s3 = [ 1, 2, 3 ];
seq<int> s4 = [t: int ];
```
<br>

Once we have a sequence, we can query different properties of that sequence. The syntax `s5[i]` can be used to retrieve the element at index `i` from sequence `s5`. The notation `s5.head` is shorthand for `s5[0]`. The length of a sequence `s5` can be obtained by using the notation `|s5|`. Two sequences can be compared using the `==` operator where they are equal iff they are of the same length and the elements at the same indices are equal.

<!-- testBlock Pass -->
```pvl
seq<int> s5 = [ 1, 2, 4, 8, 16 ];
assert s5[3] == 8;
assert |s5| == 5;
assert s5 == seq<int> { 1, 2, 4, 8, 16 };
```
<br>

## Constructing sequences from existing sequences
As mentioned above sequences are immutable, however it is possible to construct a new sequence from an existing sequence.

Elements can be added to a sequence in two ways. The first way is by concatenating two sequences `s6 + s7`. This expression represents a new sequence with the elements of `s6` followed by the elements of `s7`. The second way is to add a single value to the front of a sequence. The syntax `e::s6` is used to prepend `e` at the front of `s6`.

<!-- testBlock Pass -->
```pvl
seq<int> s6 = [ 1, 2, 4, 8, 16 ];
assert 0::s6 == [ 0, 1, 2, 4, 8, 16 ];

seq<int> s7 = [ 32, 64, 128 ];
assert s6 + s7 == [ 1, 2, 4, 8, 16, 32, 64, 128 ];
```

It is also possible to take a subsequence from an existing sequence. The syntax `s8[i..j]` is used to take the elements from `s8` from index `i` to index `j` (exclusive). By omitting either the lower bound or upper bound, one can take or drop from a sequence. The notation `s8.tail` can be used as a shorthand for `s8[1..]`.

<!-- testBlock Pass -->
```pvl
seq<int> s8 = [ 1, 2, 4, 8, 16 ];
assert s8[1..4] == [ 2, 4, 8 ];
assert s8[..2] == [ 1, 2 ];
assert s8.tail == s8[1..]; 
```

## Examples
### Sortedness
Sortedness is a property that is often used in the verification of sorting algorithms. The sortedness property for a sequence of integers could be defined as follows:

<!-- testMethod Pass -->
```pvl
pure boolean sorted(seq<int> xs) = (\forall int i ; 0 <= i && i < |xs|-1; xs[i] <= xs[i+1]);
```

### Distinct Element
Another property on sequences is the uniqueness of the elements. This property could be expressed for a sequence of integers as follows: 

<!-- testMethod Pass -->
```pvl
pure boolean distinct(seq<int> s) =
    (\forall int i; 0 <= i && i < s.length; 
        (\forall int j; 0 <= j && j < s.length && s[i] == s[j]; i == j)
    );
```

### Maximum element
Recursive functions are often used to transform or reduce a sequence. The example below goes over a sequence to get its maximum value. This function could be defined for a sequence of integers as follows:

<!-- testMethod Pass -->
```pvl
requires |xs| > 0;
ensures (\forall int i; 0 <= i && i < |xs|; xs[i] <= \result);
pure static int max(seq<int> xs) =
    1 == |xs| ?
        xs[0]:
        (xs[0] > max(xs[1..]) ?
            xs[0]:
            max(xs[1..]
        )
);
```

# Set 
Sets are an unordered collection with unique values. Sets are finite and immutable (i.e. once created they cannot be altered).

Similar to sequences, there are two ways to construct a set: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the set explicitly defined. For example, `s1` is a set of integers initialized with the values 1, 2 and 3 and `s2` is an empty set of integers.

<!-- testBlock Pass -->
```pvl
set<int> s1 = set<int> { 1, 2, 3, 2 };
set<int> s2 = set<int> { };
```

The implicit syntax is a shorter syntax. If the set is initialized with at least one value (using the implicit syntax), VerCors infers the type of the set. An empty set can be constructed by providing the type of the set. For example, `s3` is equivalent to `s1` and `s4` is equivalent to `s2`. Notice how there is no space between `{` and `t`, this is mandated by the VerCors grammar.

<!-- testBlock Pass -->
```pvl
set<int> s3 = { 1, 2, 2, 3 };
set<int> s4 = {t: int };
```

Once we have a set, we can query different properties of that set. The length of a set `s5` can be obtained by using the notation `|s5|`. Two set `s6` and `s7` can be compared using the `==` operator where they are equal iff all elements of `s6` are in `s7` and all elements of `s7` are in `s6`. The syntax `e1 \in s8` is used to check if set `s8` contains the element `e1`. The `<` and `<=` operators denote the strict subset and subset operators respectively.

<!-- testBlock Pass -->
```pvl
set<int> s5 = { 1, 2, 2, 3 };
set<int> s6 = { 3, 4, 5, 6 };
set<int> s7 = { 1, 2 };
set<int> s8 = { 2, 3 };
int e1 = 3;

assert |s5| == 3;
assert s6 != s7;
assert e1 \in s8;
assert s8 < s5;
```

## Constructing sets from existing sets
As mentioned above sets are immutable, however it is possible to construct a new set from an existing set.

There are several operations defined on sets that are part of set theory. The union of two sets is denoted by `s5 + s6`, the difference between two sets is denoted by `s5 - s6` and the intersection of two sets is denoted by `s5 * s6`. 

<!-- testBlock Pass -->
```pvl
set<int> s5 = { 1, 2, 2, 3 };
set<int> s6 = { 3, 4, 5, 6 };

assert s5 + s6 == { 1, 2, 3, 4, 5, 6 };
assert s5 - s6 == { 1, 2 };
assert s6 - s5 == { 4, 5, 6};
assert s5 * s6 == { 3 };
```

## Set comprehension

An advanced way to create a set is using *set comprehension*. The syntax is `set<T> { main | variables; selector }` and consists of three parts: the `main`, the `variables` and the `selector`.

The `variables` are the variables that are quantified over and these variables can be bound or unbound. From the quantified variables, we can select specific values by using the `selector` expression. This is a Boolean expression that selects (a part of) the quantified variables. With the selected set of variables to quantify over, we express the value that is going to be part of the resulting set using the `main` expression.

For example, we can construct the set of all even integers from 0 to 9 as follows:

```
set<int> {x | int x <- {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; x % 2 == 0};
```

To use more complex `main` expressions (i.e. non-identity functions), it is recommended to wrap the expression in a function and use that function in the `main` expression. For example, suppose we have a set of integers from 0 to 5 (inclusive) and we want to construct the set of integers where each element is doubled, we could use set comprehension as follows:

<!-- test Pass -->
```pvl
class SetComp {
    requires 0 <= j && j < 5;
    void myMethod(int j) {
       set<int> a = set<int> {SetComp.plus(x, x) | int x; x >= 0 && x <= 5 };
       assert plus(1, 1) in a; 
       assert plus(j, j) in a; 
    }

    pure static int plus(int a, int b) = a+b;
}
```

Here we define a function `plus` to wrap the expression `a+b` and use an invokation of the `plus` function as the `main` of our set comprehension.

# Bag
A bag (also called a multiset) is an unordered collection. They are equivalent to sequences without order, or sets with duplicates. Bags are finite and immutable (i.e. once created they cannot be altered).

Similar to sequences and sets, there are two ways to construct a bag: the explicit syntax and the implicit syntax. The explicit syntax requires the type of the bag explicitly defined. For example, `b1` is a bag of integers initialized with the values 1, 2, 2 and 3 and `b2` is an empty bag of integers.

<!-- testBlock Pass -->
```pvl
bag<int> b1 = bag<int> { 1, 2, 3, 2 };
bag<int> b2 = bag<int> { };
```

The implicit syntax is a shorter syntax. If the bag is initialized with at least one value (using the implicit syntax), VerCors infers the type of the bag. An empty bag can be constructed by providing the type of the bag. For example, `b3` is equivalent to `b1` and `b4` is equivalent to `b2`. Notice how there is no space between `b{` and `t`, this is mandated by the VerCors grammar.

<!-- testBlock Pass -->
```pvl
bag<int> b3 = b{ 1, 2, 2, 3 };
bag<int> b4 = b{t: int };
```

Once we have a bag, we can query different properties of that bag. The length of a bag `b5` can be obtained by using the notation `|b5|`. The syntax `e1 \in b6` is used to get the multiplicity (or number of occurrences) of an element `e1` in the bag `b6`. Two bags `b7` and `b8` can be compared using the `==` operator where they are equal iff for all elements `e2`, the multiplicity of `e2` in `b7` and `b8` are equal. The `<` and `<=` operators denote the strict subset and subset operators respectively.

<!-- testBlock Pass -->
```pvl
bag<int> b5 = b{ 1, 2, 2, 3 };
bag<int> b6 = b{ 3, 4, 5, 6, 5 };
bag<int> b7 = b{ 1, 2, 3, 2, 2, 6 };
bag<int> b8 = b{ 6, 1, 2, 2, 2, 3 };
int e1 = 5;


assert |b5| == 4;
assert (e1 \in b6) == 2;
assert b5 <= b7 && b5 < b8;
assert b7 == b8;
```

## Constructing bags from existing bags
As mentioned above bags are immutable, however it is possible to construct a new bag from an existing bag.

The union of two bags is denoted by `b9 + b10`, the difference between two bags is denoted by `b11 - b12` and the intersection of two bags is denoted by `b13 * b14`. 

<!-- testBlock Pass -->
```pvl
bag<int> b9 = bag<int> { 3 };
bag<int> b10 = bag<int> { 3, 4 };
bag<int> b11 = bag<int> { 1, 2, 2, 3 };
bag<int> b12 = bag<int> { 2, 3, 3, 4 };
bag<int> b13 = bag<int> { 1, 1, 2, 3 };
bag<int> b14 = bag<int> { 2, 3, 3, 4 };

assert b9 + b10 == bag<int> { 3, 3, 4 };
assert b12 - b11 == bag<int> { 3, 4 };
assert b11 - b12 == bag<int> { 1, 2 };
assert b13 * b14 == bag<int> { 2, 3 };
```

## Examples
`TODO`

# Map 
Maps are an unordered, collection of key/value pairs with unique keys. Maps are finite and immutable (i.e. once created they cannot be altered).

A map can be constructed using the syntax `map<K,V> { k1 -> v1, k2 -> v2, ...}`. This syntax constructs a map with keys/value pairs `(k1, v1)` and `(k2, v2)` (of type `K` and type `V` respectively). An empty map can be constructed by declaring no key/value pair.

<!-- testBlock Pass -->
```pvl
map<int, boolean> m1 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false};
map<int, boolean> m2 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false, 1 -> false, 1 -> true};
assert m1 == m2;
```

Once we have a map, we can query different properties of that map. Given a key `k1`, we can get its associated value in map `m1` using the syntax `m1[k1]` or `m1.get(k1)`. The cardinality/size of the map can be queried using the syntax `|m1|` or `m1.size`. The size of a map is equivalent to the size of its key set. The key, value and key/value pair sets can be obtained using the notations `m1.keys`, `m1.values` and `m1.items` respectively.

<!-- testBlock Pass -->
```pvl
map<int, boolean> m1 = map<int,boolean>{1 -> true, 2 -> true, 0 -> false};

assert |m1| == 3;
assert m1[0] == false;
assert m1[1] == true;
assert m1[2] == true;

assert m1.keys == { 1, 2, 0 };
assert m1.values == { true, false };
assert tuple<int, boolean> { 0, false } \in m1.items;
assert tuple<int, boolean> { 1, true } \in m1.items;
assert tuple<int, boolean> { 2, true } \in m1.items;
```

We can add a key/value pair `(k4, v4)` to the map `m4` using the syntax `m4.add(k4, v4)`. If the key was already present in `m4`, its value gets updated. We can also remove a key `k5` from a map `m5` using the function `m5.remove(k5)`.

<!-- testBlock Pass -->
```pvl
map<int, int> m1 = map<int,int>{};
map<int, int> m2 = m1.add(1, 1).add(2, 4).add(3, 9);
map<int, int> m3 = m2.remove(2);
map<int, int> m4 = m3.remove(3).remove(1);

assert |m1| == 0;
assert m2[1] == 1;
assert m2[2] == 4;
assert m2[3] == 9;

assert !(2 \in m3.keys);
assert m3[1] == 1;
assert m3[3] == 9;

assert |m4| == 0;
```

## Examples
`TODO`



# Tuple
A tuple is an ordered, immutable collection containing exactly two elements.

A tuple can be constructed using the syntax `tuple<F,S> { fst, snd }`. This syntax constructs a tuple with the first value `fst` of type `F` and the second value `snd` of type `S`. A tuple can also be deconstructed into its first and second value by using the functions `t2.fst` and `t2.snd` respectively. For example, a tuple `t1` with values `(1, false)` is constructed as:

<!-- testBlock Pass -->
```pvl
tuple<int, boolean> t1 = tuple<int, boolean> { 1, false };
assert t1.fst == 1;
assert t1.snd == false;
```

## Examples
`TODO`







# Option
The option data type is a container that either represents the presence of an element in the container or the absence of it.

An option type can be constructed with the constructors `Some(e)` or `None`. The constructor `Some(e)` represents the presence of the value `e` in the option type and the constructor `None` represents the absence of an element.

<!-- testBlock Pass -->
```pvl
option<int> o1 = None;
option<int> o2 = Some(3);
```

Option types can be compared to each other where two options `o3` and `o4` are equivalent iff they both contain an element `e3` and `e4` respectively and `e3` equals `e4`, or both are empty.

<!-- testBlock Pass -->
```pvl
option<int> o3 = Some(6);
option<int> o4 = Some(6);
option<int> o5 = Some(1);
option<int> o6 = None;

assert o3 == o4;
assert o4 != o5;
assert o5 != o6;
```

## Examples
`TODO`










# ADT Reference
The tables below are a reference for all the functions/operations that are defined on the different ADTs.

## Sequence 
Short Description | Return type | Syntax
----------------- | ----------- | -------------
Constructor | `seq<T>` | `seq<T> { e1, e2, ... }`<br>Constructs a sequence with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the sequence is not initialized, an empty sequence is constructed.
Constructor | `seq<T>` | `[ e1, e2, ... ]`<br>Constructs a sequence with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the sequence to be initialized.
Constructor | `seq<T>` | `[t: T ]`<br>Constructs an empty sequence with element of type `T`
Length | `int` | `\|s1\|` or `s1.size` <br>Returns the length/cardinality of the sequence `s1`
Empty | `boolean` | `s1.isEmpty`<br>Returns whether `|s1| == 0`
Comparison | `boolean` | `s1 == s2`<br>Returns `true` if `s1` and `s2` are equivalent
Concatenation | `seq<T>` | `s1 + s2` or `s1.concat(s2)`<br>Denotes the sequence with elements from `s1` followed by the elements of `s2`
Contains | `boolean` | `e \in xs` or `xs.contains(e)`. True if `e` is in `xs`. 
Indexing | `T` | `s1[i]`<br>Returns the element at index `i` of sequence `s1`
Head | `T` | `s1.head`<br>Returns the first element of sequence `s1`
Tail | `seq<T>` | `s1.tail`<br>Denotes the sequence with the elements from `s1` excluding the first element
Prepend | `seq<T>` | `x::xs` or `xs.prepend(x)`<br>Denotes the sequence with elements of `xs` prepended with the element `x`
Slicing | `seq<T>` | `s1[i..j]` or `s1.slice(i, j)`<br>Denotes the subsequence of sequence `s1` from index `i` until index `j` (exclusive)
Dropping | `seq<T>` | `s1[i..]` or `s1.drop(i)`<br>Denotes the subsequence starting at `i`
Taking | `seq`<T>` | `s1[..j]` or `s1.take(j)`<br>Denotes the subsequence of the first `j` elements
Updating | `seq<T>` | `s1[i -> v]` or `s1.update(i, v)`<br>Denotes the sequence with elements from `s1` where index `i` has been updated to value `v` 
Removing | `seq`<T> | `s1.removeAt(i)`<br>Denotes the sequence where the element at index `i` is removed. Equivalent to `s1[..i] + s1[i+1..]`
Summation | int | `(\sum int i; low <=i && i< up; s1[i]);`<br>Sum the elements of a sequence of integers `s1` between the indices `low` and `up` (exclusive) 

## Set
Short Description | Return type | Syntax
----------------- | ------------- | -------------
Constructor | `set<T>` | `set<T> { e1, e2, ... }`<br>Constructs a set with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the set is not initialized, an empty set is constructed.
Constructor | `set<T>` | `{ e1, e2, ... }`<br>Constructs a set with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the set to be initiliazed.
Constructor | `set<T>` | `{t: T }`<br>Constructs an empty set with element of type `T`
Length | `int` | `\|s1\|` or `s1.size`<br>Returns the length/cardinality of the set `s1` 
Empty | `boolean` | `s1.isEmpty`<br>Returns whether `|s1| == 0`
Comparison | `boolean` | `s1 == s2`<br>Returns `true` if `s1` and `s2` are equivalent
Membership | `boolean` | `e \in s1` or `s1.contains(e)`<br>Returns `true` if the value `e` is in the set `s1`
Set Union | `set<T>` | `s1 + s2` or `s1.union(s2)`<br>Denotes the set of all elements from sets `s1` and `s2` of the same type `T`
Set Difference | `set<T>` | `s1 - s2` or `s1.difference(s2)`<br>Denotes the set of all elements from set `s1` that are not in set `s2`
Subset | `boolean` | `s1 <= s2` or `s1.subsetOf(s2)`<br>Returns `true` if set `s1` is a subset of set `s2`
Strict Subset | `boolean` | `s1 < s2` or `s1.strictSubsetOf(s2)`<br>Returns `true` if set `s1` is a strict subset of set `s2`
Intersection |`set<T>` | `s1 * s2` or `s1.intersect(s2)`<br>Denotes the set of all elements that are both in sets `s1` and `s2`
Set Comprehension | `set<T>` | `set<T> { main \| variables; selector }`<br>Constructs a set of elements of the form `main` over the quantified variables in `variables` that match `selector`


## Bag
Short Description | Return type | Syntax
----------------- | ----------- | -------------
Constructor | `bag<T>` | `bag<T> { e1, e2, ... }`<br>Constructs a bag with elements of type `T` initiliazed with values `e1`, `e2`, etc. When the bag is not initialized, an empty bag is constructed.
Constructor | `bag<T>` | `b{ e1, e2, ... }`<br>Constructs a bag with elements of type `T` initiliazed with values `e1`, `e2`, etc. This syntax requires the bag to be initiliazed.
Constructor | `bag<T>` | `b{t: T }`<br>Constructs an empty bag with element of type `T`
Length | `int` | `\|b1\|` or `b1.size`<br>Returns the length/cardinality of the bag `b1` 
Empty | `boolean` | `b1.isEmpty`<br>Returns whether `|b1| == 0`
Multiplicity | `int` | `e \in b1` or `b1.count(e)`<br>Returns the number of occurrences of value `e` in bag `b1`
Comparison | `boolean` | `b1 == b2`<br>Returns `true` if `b1` and `b2` are equivalent
Bag Union | `bag<T>` | `b1 + b2` or `b1.sum(b2)`<br>Denotes the bag of all elements from bags `b1` and `b2` of the same type `T`
Bag Difference | `bag<T>` | `b1 - b2` or `b1.difference(b2)`<br>Denotes the bag of all elements from bag `b1` that are not in bag `b2`
Subset | `boolean` | `b1 <= b2` or `b1.subbagOf(b2)`<br>Returns `true` if bag `b1` is a subset of bag `b2`
Strict Subset | `boolean` | `b1 < b2` or `b1.strictSubbagOf(b2)`<br>Returns `true` if bag `b1` is a strict subset of bag `b2`
Intersection |`bag<T>` | `b1 * b2` or `b1.intersect(b2)`<br>Denotes the bag of all elements that are both in bags `b1` and `b2`


## Map
Short Description | Return type | Syntax
----------------- | ----------- | -------------
Constructor | `map<K,V>` | `map<K,V> { k1 -> v1, k2 -> v2, ...}`<br>Constructs a map with key-value pairs of type `K` and `V` respectively initiliazed with pairs `k1,v1`, `k2,v2`, etc. 
Build/Add | `map<K,V>` | `m1.add(k1, v1)`<br>Adds the key/value pair `(k1,v1)` to the map `m1`. If the key is already present in `m1`, update the value of the key.
GetByKey | `V` | `m1.get(k1)` or `map[k1]`<br>Gets the value mapped by the key `k1` from the map `m1`.
Remove | `map<K,V>` | `m1.remove(k1)`<br>Removes the key `k1` and its associated value from the map `m1`.
Length | `int` | `m1.size` or `\|m1\|`<br>Returns the length/cardinality of the map `m1` 
Empty | `boolean` | `m1.isEmpty`<br>Returns whether `|m1| == 0`
Comparison | `boolean` | `m1.equals(m2)` or `m1 == m2`<br>Returns `true` if the keysets of `m1` and `m2` are equivalent and the keys map to the same values.
Key Set | `set<K>` | `m1.keys`<br>Returns a set of keys in map `m1`
Value Set | `set<V>` | `m1.values`<br>Returns a set of the values in map `m1`
Item Set | `set<tuple<K,V>>` | `m1.items`<br>Returns a set of tuples corresponding to the key-value pairs in map `m1`
Disjoint | `boolean` | `m1.disjoint(m2)`<br>Returns `true` if no key is in both the key set of `m1` and the key set of `m2`.


## Tuple
Short Description | Return type | Syntax
----------------- | ----------- | -------------
Constructor | `tuple<F,S>` | `tuple<F,S> {fst, snd}`<br>Construct a tuple with first element `fst` (of type `F`) and second element `snd` (of type `S`)
Get First Element | `F` | `t.fst`<br> Get the first element of the tuple `t` (of type `tuple<F,S>`)
Get Second Element | `S` | `t.snd`<br> Get the second element of the tuple `t` (of type `tuple<F,S>`)

## Option
Short Description | Return type | Syntax
----------------- | ----------- | -------------
Constructor | `option<T>` | `Some(e)`<br> Constructs an option which contains the element `e` of type `T`
Constructor | `option<T>` | `None`<br> Returns the option `None`
Getter | `T` | `e.get`<br>Returns the value contained in the option if it is filled
Getter | `T` | `e.getOrElse(t)`<br>Returns the value contained in the option, `t` otherwise
Comparison | `boolean` | `o1 == o2` <br> Returns `true` if the element contained in the option `o1` is equivalent to the element wrapped in the option `o2`, or both are empty

# Custom ADTs

ADTs can be useful to provide VerCors with domain-specific assumptions. For example, a custom int-tuple ADT can be defined in PVL as follows:

```java

adt MyTuple {
  pure MyTuple cons(int l, int r);
  pure int left(MyTuple t);
  pure int right(MyTuple t);

  axiom (\forall int l, int r; left(cons(l, r)) == l);
  axiom (\forall int l, int r; right(cons(l, r)) == r);
  axiom (\forall int l1, int l2, int r1, int r2; 
    (cons(l1, r1) == cons(l2, r2)) ==> (l1 == l2 && r1 == r2));
}

void testTuple(MyTuple t) {
  assert MyTuple.cons(1, 2) == MyTuple.cons(1, 2);
  assert MyTuple.cons(1, 2) != MyTuple.cons(3, 4);
}
```

Note however that it is easy to make mistakes and define axioms from which false can be derived. If this happens, and your custom ADT is used in your code or contracts, from that point on VerCors assumes false, which makes every proof obligation after that point trivial to prove. Furthermore, when writing quantifiers in ADTs it is important to also define triggers. VerCors and its backend can often infer some trigger, but these are usually suboptimal.

Custom ADTs are supported in all frontends.