diff options
| author |  leino <unknown> | 2015-04-05 01:56:49 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-05 01:56:49 -0700 |
| commit | e9c7c508c1900e6195164d263c9249e3c7b56b51 (patch) | |
| tree | 015bbdd42d118838ed4d2a758444d7e1eb55d46b /Binaries | |
| parent | cee337934c619bfeb646d83243eff1f08e83902d (diff) | |
Fixed some bugs in override axioms (but still missing support for classes with type parameters).
Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 |
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 ----------------------------------------
// ---------------------------------------------------------------
|