summaryrefslogtreecommitdiff
path: root/Test/dafny0/Datatypes.dfy
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Allow "match" expressions anywhereGravatar Rustan Leino2014-01-03
* Fixed a problem where changes to a substMap were not being undone, curing Iss...Gravatar Rustan Leino2013-06-20
* One more test case for the "datatype constructor cases" axiom, namely the exa...Gravatar Rustan Leino2013-06-20
* Make "datatype constructor cases" axiom available whenever the discriminator ...Gravatar Rustan Leino2013-06-20
* Added a test case for "all cases of a datatype"Gravatar Unknown2012-10-17
* Dafny: updated test suite to new syntaxGravatar Jason Koenig2012-07-30
* Dafny: for a datatype with just one constructor, don't check (but do assume) ...Gravatar Rustan Leino2011-12-19
* Dafny: implemented the wellformedness check that datatype destructors are onl...Gravatar Rustan Leino2011-11-11
* Dafny: fixed parsing bug with "!in"Gravatar Rustan Leino2011-09-08
* Dafny: added implicit datatype query fields and datatype destructor fieldsGravatar Rustan Leino2011-06-05
* Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* Dafny:Gravatar Rustan Leino2011-05-21
* Dafny: support for nested match expressionsGravatar rustanleino2011-03-01
* Dafny:Gravatar rustanleino2011-02-17
* Added wellformedness checks to method specificationsGravatar rustanleino2010-03-12
* * Added decreases clauses to functionsGravatar rustanleino2009-11-24
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* Swapped previous file (Datatypes.bpl) for the correct test file (Datatypes.dfy).Gravatar rustanleino2009-11-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 19:24:42 +0000