Added resolution and translation of algebraic datatypes and (in function bodies) match expressions.

Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.

1 files changed, 5 insertions, 0 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 4e524175..06b33b86 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -192,6 +192,11 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type DatatypeType;

 

+type DtCtorId;

+function DatatypeCtorId(DatatypeType) returns (DtCtorId);

+

+function DtRank(DatatypeType) returns (int);

+

 // ---------------------------------------------------------------

 

 type Field alpha;