summaryrefslogtreecommitdiff
path: root/Test/dafny3/Streams.dfy
Commit message (Collapse)AuthorAge
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
|
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵Gravatar Rustan Leino2014-02-23
| | | | -> "prefix lemma")
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no ↵Gravatar Rustan Leino2013-06-29
| | | | longer to to functions with ensures clauses
* Renamed "parallel" statement to "forall" statement, and made the parentheses ↵Gravatar Rustan Leino2013-03-06
| | | | around the bound variables optional.
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
| | | | Added syntactic support for codatatype #-form equalities.
* Test cases for co-inductive proofs, and an axiom that makes some of them ↵Gravatar Rustan Leino2012-10-19
possible