summaryrefslogtreecommitdiff
path: root/Test/dafny3/SimpleInduction.dfy
Commit message (Collapse)AuthorAge
* Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ↵Gravatar Rustan Leino2015-07-28
| | | | | | time) in the test suite. Removed some assertions that have been rendered unnecessary because of the computations that Dafny instructs the SMT solver to do.
* 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
|
* Renamed "parallel" statement to "forall" statement, and made the parentheses ↵Gravatar Rustan Leino2013-03-06
| | | | around the bound variables optional.
* Examples from co-induction paperGravatar Rustan Leino2013-01-22