Set operations unsupported in dafny

Question

I am new in dafny and I encountered a problem when working with a set like this one: var myset : set<(int, int)> := {(1, 10), (2, 20), (3, 20)};

How can I get first pair into a variable? And then how can I access each value inside this pair?
How can I add a pair to my myset ?

For arrays is working in this way : myarray[i].0 and myarray[i].1.

user_438267 · Answer

Sets are immutable, unordered collections.

There is no such thing as the "first" element of the set. You can choose an arbitrary element like this:
```
var x :| x in myset;  // get an arbitrary element
```
x is guaranteed to be an element of the set, but you don't know which one. For example, Dafny verifies the following assertion about x:
```
assert x == (1,10) || x == (2, 20) || x == (3, 20);
```
To add an element, you can use + (and variable assignment):
```
myset := myset + {(4, 0)}; // add an element
```