Destructuring Syntax for Tuples?

user_764576 0
Viewed 26

So, I'm wondering whether there is any support for destructuring syntax in Dafny. Something along the following lines:

function method f(x:int) : (int,int) { (x,x+1) }

method test() {
    var y:int;
    var z:int;
    (y,z) := f(1);
}

In fact, I want to go further than this as I want to destructure within a function.

dafny
1 Answers

According to the reference manual, you cannot do it for assignment statements, but only for variable declaration statements, like this:

function method f(x:int) : (int,int) { (x,x+1) }

method test() {
    var (y,z) := f(1);
}

If you want to annotate the types, you can do it like this:

var (y:int, z:int) := f(1);

You can also use a let expression to do this inside a function, like this:

function method f(x:int) : (int,int) { (x,x+1) }

function g() {
    var (y,z) := f(1);
    y+z
}
user_4382670
Related