diff options
author | rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
commit | 17efb869d2b4a00c26e04b27de34b8bc643ad581 (patch) | |
tree | a9368d57c7f5fe58b7a66ce08e12fe1c8e6e9912 /Binaries | |
parent | 2efa59dea051803bc716d02070aa013397cfccc4 (diff) |
Start (some parsing and resolution) of adding algebraic datatypes to Dafny.
Included VSI-Benchmarks in standard tests.
Diffstat (limited to 'Binaries')
-rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 4eee233b..4e524175 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -190,6 +190,10 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } // ---------------------------------------------------------------
+type DatatypeType;
+
+// ---------------------------------------------------------------
+
type Field alpha;
type HeapType = <alpha>[ref,Field alpha]alpha;
|