summaryrefslogtreecommitdiff
path: root/Test/dafny3/GenericSort.dfy
Commit message (Expand)AuthorAge
* Mark old "import A as B" syntax as deprecated. The new syntax is "import A : B"Gravatar qunyanm2016-02-02
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
* Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Another variation of GenericSort, this time instantiating with "int"Gravatar Rustan Leino2014-07-14
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
* Added test3/GenericSort.dfy, which shows how modules can be used to write and...Gravatar Rustan Leino2013-12-18