From 9ed23deb0a3db4b61cf07fc6b551e10bc5436837 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 20 Nov 2009 23:04:27 +0000
Subject: 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.

---
 Binaries/DafnyPrelude.bpl | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Binaries')

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;
-- 
cgit v1.2.3