summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-07-16 17:22:18 -0700
committerGravatar Rustan Leino <unknown>2013-07-16 17:22:18 -0700
commitb0bb7bf96406d8695d5ec2377d9ce2b2acba44f0 (patch)
tree6d1b5d1f3c79968ce8bc8900337804c849905212
parent5e7d25359f1bd5425d5400019bfe08bcc87fb30f (diff)
Syntactic improvements in two tests.
-rw-r--r--Test/dafny3/Filter.dfy2
-rw-r--r--Test/dafny3/Paulson.dfy2
2 files changed, 2 insertions, 2 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)) {
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index c1721af3..431ff543 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -150,7 +150,7 @@ ghost method Example7<A>(f: FunctionHandle<LList<A>>)
// Given the definition of h, prove h(f, _) == Iterates(f, _):
ensures forall M :: h(f, M) == Iterates(f, M);
{
- forall (M) {
+ forall M {
BisimulationLemma(0, f, M);
}
}