blob: 3f95ce9fa80412171345b61270002b9a1fe3b6da (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
// RUN: %dafny /autoTriggers:1 /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
predicate P(e:int, p:int) { true }
predicate Q(i:int, t:int)
lemma Tester(x:int)
{
assert forall i :: Q(i, x) ==> (forall p {:trigger P(i, p)} :: P(i, p));
}
|
