diff options
| author |  chmaria <unknown> | 2014-06-03 16:55:05 -0700 |
|---|---|---|
| committer | chmaria <unknown> | 2014-06-03 16:55:05 -0700 |
| commit | 6d32fe37e3d343f9e310eeea193efc8da5982600 (patch) | |
| tree | 3a6bcda5eb3ef99b9e2e8fd030f3352ab2296476 /Test/dafny0/ResolutionErrors.dfy.expect | |
| parent | 607ef28aadb281ab61a2be493a637126e967a388 (diff) | |
Added support for 'dirty' forall statements.
One can now write forall statements without bodies
(but with ensures clauses) as follows:
forall s | s in S ensures s < 0;
where S is set<int>.
The ensures clauses are assumed but not checked.
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index eb9b244b..2c0664d9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -132,4 +132,5 @@ ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
-134 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\ResolutionErrors.dfy
+ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
+135 resolution/type errors detected in ResolutionErrors.dfy
|