summaryrefslogtreecommitdiff
path: root/Test/hofs/Field.dfy.expect
Commit message (Collapse)AuthorAge
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
| | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests.
* Snapshot, to be continuedGravatar leino2014-12-02
|
* Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
* The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter