如何使用“存在”量词？

Question

Dafny 文档没有使用“存在”量词。

method Main() {
    assert (exists n: int :: n > 1);
}

这会产生一个 AssertionError

Answer 1

以下作品：

predicate dummy(n: int) {true}

method Main() {
    assert dummy(2);
    assert (exists n : int {:trigger dummy(n)} :: n > 1);
}

对于任何整数m > 1，您可以将dummy(2) 替换为dummy(m)。

这个答案不是很好，因为我不能确切地告诉你为什么上面的工作。但是，有关触发器的更多信息，您可以阅读this。