diff options
| author |  Rustan Leino <unknown> | 2013-07-16 17:22:18 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-16 17:22:18 -0700 |
| commit | b0bb7bf96406d8695d5ec2377d9ce2b2acba44f0 (patch) | |
| tree | 6d1b5d1f3c79968ce8bc8900337804c849905212 /Test/dafny3/Filter.dfy | |
| parent | 5e7d25359f1bd5425d5400019bfe08bcc87fb30f (diff) | |
Syntactic improvements in two tests.
Diffstat (limited to 'Test/dafny3/Filter.dfy')
| -rw-r--r-- | Test/dafny3/Filter.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy index d45f4acc..287b4006 100644 --- a/Test/dafny3/Filter.dfy +++ b/Test/dafny3/Filter.dfy @@ -164,7 +164,7 @@ ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle) requires AlwaysAnother(s, h);
ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h);
{
- forall (x)
+ forall x
ensures In(x, Filter(s, h)) <==> In(x, s) && P(x, h);
{
if In(x, Filter(s, h)) {
|