summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl5
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;