Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix: Unify column numbers in Dafny's errors | Clément Pit--Claudel | 2015-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. | ||
* | Use arbitrary lookahead to determine if the next expression is a lambda ↵ | leino | 2014-11-13 |
| | | | | expression. | ||
* | Add higher-order-functions and some other goodies | Dan Rosén | 2014-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 |