summaryrefslogtreecommitdiff
path: root/Test/dafny0/CoPrefix.dfy
Commit message (Collapse)AuthorAge
* 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.)