summaryrefslogtreecommitdiff
path: root/Test/dafny0/Coinductive.dfy
Commit message (Expand)AuthorAge
* Added "inductive lemma" methodsGravatar leino2015-05-07
* Added inductive predicatesGravatar leino2015-05-06
* 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
* Fixed some checking of recursive method/copredicate callsGravatar Rustan Leino2014-02-23
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -...Gravatar Rustan Leino2014-02-23
* Allow co-predicates to be wrapped inside bounded existential quantifiersGravatar Rustan Leino2013-08-04
* Fixed the problem with the previous check-in.Gravatar Rustan Leino2013-01-18
* Change the encoding of proof certificates to make the two levels explicitGravatar Unknown2012-10-12
* Dafny: added copredicatesGravatar Rustan Leino2012-07-03
* Dafny: added resolution tests cases for inductive datatypesGravatar Unknown2012-04-27
* Dafny: fixed resolution bug for inductive datatypes (previous check did not h...Gravatar Unknown2012-04-25