破坏该元组的语法？

Question

因此，我想知道是否有任何支持Dafny中破坏语法的支持。沿着以下几行：

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

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

实际上，我想走得更远，因为我想在函数中破坏。

Answer 1

根据参考手册但是仅对于可变声明语句，例如：

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

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

如果要注释这些类型，则可以这样做：

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

您也可以使用Let Expression在函数中执行此操作，例如：

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

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