summaryrefslogtreecommitdiff
path: root/Test/dafny0/CoPrefix.dfy
Commit message (Collapse)AuthorAge
* Additional testsGravatar leino2015-09-28
|
* 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")
* Renamed "parallel" statement to "forall" statement, and made the parentheses ↵Gravatar Rustan Leino2013-03-06
| | | | around the bound variables optional.
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
|
* Fixed the problem with the previous check-in.Gravatar Rustan Leino2013-01-18
|
* Some additional resolution checks for co stuff.Gravatar Unknown2013-01-18
| | | | Beefed up some test cases.
* Encode codatatype equalities by predefined copredicates, including their ↵Gravatar Rustan Leino2013-01-15
| | | | prefix versions
* Support for copredicates and prefix predicates in comethods.Gravatar Rustan Leino2012-12-04
(Missing from the co support are (prefix) equalities of codatatypes, various restrictions on the use of co/prefix-predicates, and tactic support for applying the (prefix-)induction automatically.)