summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl7
1 files changed, 7 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 4972517b..74bdb63e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -101,6 +101,13 @@ type ref;
const null: ref;
// ---------------------------------------------------------------
+// -- Traits -----------------------------------------------------
+// ---------------------------------------------------------------
+
+const unique NoTraitAtAll: ClassName;
+function TraitParent(ClassName): ClassName;
+
+// ---------------------------------------------------------------
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------