diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-02-18 15:58:13 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-02-18 15:58:13 -0800 |
| commit | 5b6de79e16850e70a9ab1a37ba45245275c3fd20 (patch) | |
| tree | 7284d7e9575e9f95b762e12a809be2ebdfabbae4 /Test/dafny0/RefinementErrors.dfy | |
| parent | 35e2020655eea10acdb902f4320952e281f28967 (diff) | |
Dafny: added syntactic support for ...'s in statements, and started implementation of refinement transformations thereof
Diffstat (limited to 'Test/dafny0/RefinementErrors.dfy')
| -rw-r--r-- | Test/dafny0/RefinementErrors.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/RefinementErrors.dfy b/Test/dafny0/RefinementErrors.dfy index 25ba94ad..df6f1a71 100644 --- a/Test/dafny0/RefinementErrors.dfy +++ b/Test/dafny0/RefinementErrors.dfy @@ -44,7 +44,7 @@ module B refines A { { // yes, can give it a body } method FullBodied(x: int) returns (y: bool, k: seq<set<object>>) - { // error: not allowed to change body (not yet implemented) + { } } } |