blob: 878ed57ad9b8b44133070090844689f5896e5d32 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
predicate P(i:int) { true }
lemma Tester()
{
// forall i ensures false ==> P(i) {}
forall i ensures P(i) <== false {}
assert forall i :: P(i) ==> false;
assert P(0);
assert false;
}
|