summaryrefslogtreecommitdiff
path: root/Source/Dafny/Printer.cs
Commit message (Expand)AuthorAge
* DafnyExtension: Worked on integrating the verification result caching.Gravatar wuestholz2013-06-06
* Made the semi-colon after "type" and "module" declarations optional.Gravatar Rustan Leino2013-05-10
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Beefed up assign/let-such-that to generate possible witnesses for set/multise...Gravatar Rustan Leino2013-03-25
* Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
* Added the <== operator.Gravatar Nadia Polikarpova2013-03-14
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Pretty print the new parentheses-less "if" and "while" statements as such.Gravatar Rustan Leino2013-02-21
* Added Equals method on TypeGravatar Rustan Leino2013-02-20
* First take on calc expressions.Gravatar Nadia Polikarpova2013-02-14
* Added parsing and resolution of a new let-such-that expression. Translation h...Gravatar Rustan Leino2013-01-21
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
* Create prefix methods during resolution, not translation.Gravatar Unknown2013-01-18
* Some additional resolution checks for co stuff.Gravatar Unknown2013-01-18
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
* Corrected pretty printing of 'comethod'Gravatar Rustan Leino2012-11-25
* Parse prefix predicates/methodsGravatar Rustan Leino2012-11-24
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* Hover text for iterator declarations (and not for the methods they generate)Gravatar Rustan Leino2012-10-04
* Put all sources under \Source directoryGravatar Rustan Leino2012-10-04