summaryrefslogtreecommitdiff
path: root/Test/hofs/VectorUpdate.dfy.expect
Commit message (Collapse)AuthorAge
* Type parameters in method/function signatures are no longer auto-declared. ↵Gravatar Rustan Leino2015-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.
* Add the VectorUpdate exampleGravatar Dan Rosén2014-08-14