Test/triggers/nested-quantifiers-all-get-triggers.dfy


1
2
3
4
5
6
7
8
9

// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// This checks that nested quantifiers do get triggers, and that the parent
// quantifier does not get annotated twice

method M() {
  ghost var x := forall s: set<int>, x: int :: (x in s ==> forall y :: y == x ==> y in s);
}