| Commit message (Expand) | Author | Age |
* | Implement module export so we can export a subset of items defined in the | qunyanm | 2016-01-29 |
* | Implement 'extern' declaration modifier. | Richard L. Ford | 2016-01-27 |
* | Parsing and pretty printing of the new "existential guards" of the two kinds ... | leino | 2015-10-03 |
* | Refactor the error reporting code | Clément Pit--Claudel | 2015-08-18 |
* | Fix a bug with includes and /useBaseNameForFileName | Clément Pit--Claudel | 2015-07-23 |
* | multiple changes... | Michael Lowell Roberts | 2015-07-02 |
* | Add the ability to specify how much "fuel" a function should have, | Bryan Parno | 2015-07-01 |
* | Add an infinite set collection type. | qunyanm | 2015-05-29 |
* | Added "inductive lemma" methods | leino | 2015-05-07 |
* | Added inductive predicates | leino | 2015-05-06 |
* | Allow trigger annotations in more statements and expressions | chrishaw | 2015-03-11 |
* | Added 'protected' keyword (syntax) | leino | 2015-03-07 |
* | Add imap type, which is like map but may have have infinite size | chrishaw | 2015-02-26 |
* | Minor change to grammar to avoid missing token | wuestholz | 2015-01-24 |
* | Allow user-specified type parameters | leino | 2014-12-09 |
* | Snapshot, to be continued | leino | 2014-12-02 |
* | Use arbitrary lookahead to determine if the next expression is a lambda expre... | leino | 2014-11-13 |
* | Took a pass through the whole grammar to clean up allowSemi/allowLambda param... | leino | 2014-11-11 |
* | Cleaned up a number of LL(1) conflicts in the grammar (I wish Coco/R supporte... | leino | 2014-11-10 |
* | Resolved several more LL(1) warnings in the grammar | Rustan Leino | 2014-11-06 |
* | Started fixing a number of LL(1) warnings | leino | 2014-11-06 |
* | Added initial support for dirty while statements. | chmaria | 2014-11-01 |
* | Allow non-ghost axioms in order to model trusted external calls, | Bryan Parno | 2014-10-27 |
* | Allow underscores in numeric literals (and in field/destructor names that are... | leino | 2014-10-23 |
* | Add char literals. | leino | 2014-10-20 |
* | Added types "char" and "string" (the latter being a synonym for "seq<char>"). | leino | 2014-10-20 |
* | Did more refactoring. | wuestholz | 2014-09-23 |
* | Changed syntax of newtype | leino | 2014-08-26 |
* | Changed syntax of derived types to "newtype" | leino | 2014-08-21 |
* | Start of derived types (aka "new types") | leino | 2014-08-20 |
* | Merge | Dan Rosén | 2014-08-11 |
|\ |
|
* | | Add higher-order-functions and some other goodies | Dan Rosén | 2014-08-11 |
| * | added trait feature: | Reza Ahmadi | 2014-07-18 |
|/ |
|
* | Make syntax of "match" expressions and "match" statements the same -- curly b... | Rustan Leino | 2014-06-24 |
* | Added "modify" statement. | Rustan Leino | 2014-04-03 |
* | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -... | Rustan Leino | 2014-02-23 |
* | Preliminary support for reals in Dafny specs. No compiler suport yet. | Bryan Parno | 2014-02-10 |
* | Add support for the "include" keyword, which accepts a (possibly relative) path | Bryan Parno | 2013-12-10 |
* | Allow calls to side-effect-free ghost methods from expressions | Rustan Leino | 2013-08-06 |
* | Introduced keywords "lemma" (like a "ghost method", but not allowed to have a... | Rustan Leino | 2013-08-02 |
* | Add support for hexidecimal numbers. | parno | 2013-07-30 |
* | Fixed parsing bug in "if" and "while" guards | Rustan Leino | 2013-07-10 |
* | Made the semi-colon after "type" and "module" declarations optional. | Rustan Leino | 2013-05-10 |
* | The "choose" statement, hacky and specialized as it was, is now gone. Use th... | Rustan Leino | 2013-03-27 |
* | Finished support for ==# in calc, changed Paulson example to use it. | Nadia Polikarpova | 2013-03-20 |
* | Added the <== operator. | Nadia Polikarpova | 2013-03-14 |
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ... | Rustan Leino | 2013-03-06 |
* | "!!" can now be parsed as two "!". More concise parsing for "!in". | Nadia Polikarpova | 2013-02-07 |
* | Removed the syntactic form copredicate #-form with the implicit argument. | Rustan Leino | 2013-01-16 |
* | Improved error message for making the mistake of saying 'returns' instead of ... | Rustan Leino | 2012-11-25 |