| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Type parameters in method/function signatures are no longer auto-declared. ↵ |  Rustan Leino | 2015-07-02 |
| | | | | | | | | | | | | | | Although convenient and concise, the auto-declare behavior has on many occasions caused confusion when a type name has accidentally been mistyped (and Dafny had then accepted and auto-declared the name). Note, the behavior of filling in missing type parameters is still supported. This mode, although unusual (even original?) in languages, is different from the auto- declare behavior. For auto-declare, identifiers could be used in the program without having a declaration. For fill-in parameters, the implicitly declared type parameters remain anonymous. | ||
| * | Compile lambda functions and apply expressions, and change let expr compilation |  Dan Rosén | 2014-08-12 |
| | | |||
| * | 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 | |||
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |