summaryrefslogtreecommitdiff
path: root/Test/dafny3/Filter.dfy
Commit message (Collapse)AuthorAge
* Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requiresGravatar qunyanm2016-03-28
| | | | | it. Don't use pretty warning signs since we can't diff them correctly in the test output from the test run.
* Made /rewriteFocalPredicates:1 the defaultGravatar Rustan Leino2015-10-02
|
* Changed dafny3/Filter.dfy to use higher-order functions instead of the ↵Gravatar leino2015-08-12
| | | | previous function handles
* Change the induction heuristic for lemmas to also look in precondition for ↵Gravatar leino2015-08-12
| | | | | | clues about which parameters to include. As a result, improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and beautified some others.
* 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")
* Syntactic improvements in two tests.Gravatar Rustan Leino2013-07-16
|
* Added a coinductive/inductive Filter example to the test suiteGravatar Rustan Leino2013-03-18