Как использовать квантификатор «существует»?

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);
}

Вы можете заменить dummy(2) на dummy(m) для любого целого числа m > 1.

Этот ответ не велик, так как я могу 'Я не скажу вам, почему все вышеперечисленное работает. Однако, для получения дополнительной информации о триггерах вы можете прочитать this .