summaryrefslogtreecommitdiff
path: root/Test/dafny4/BinarySearch.dfy
Commit message (Collapse)AuthorAge
* Made semi-colons are specification clauses optional. In a future version, ↵Gravatar leino2014-10-25
| | | | they will no longer be allowed.
* Allow underscores in numeric literals (and in field/destructor names that ↵Gravatar leino2014-10-23
| | | | | | are written as numeric strings). The underscores have no semantic meaning, but can help a human parse the numbers.
* Fixed crash in inferred descreases clauses involving newtypes.Gravatar leino2014-10-21
Added BinarySearch as a test case.