summaryrefslogtreecommitdiff
path: root/Test/dafny0/Datatypes.dfy
Commit message (Expand)AuthorAge
* 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