summaryrefslogtreecommitdiff
path: root/Test/dafny0/DTypes.dfy
Commit message (Expand)AuthorAge
* Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Change behavior of 'decreases *', which can be applied to loops and methods. ...Gravatar Rustan Leino2014-08-19
* Allow an arbitrary-type to take type parametersGravatar Rustan Leino2014-07-15
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* Dafny:Gravatar Rustan Leino2011-05-21
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
* Dafny:Gravatar rustanleino2011-03-04
* Dafny:Gravatar rustanleino2011-02-17
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
* Introduced operator !in in Dafny. An expression "x !in S" is equivalent to "...Gravatar rustanleino2009-11-05
* Initial set of files.Gravatar mikebarnett2009-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 11:28:11 +0000