diff options
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 50433b54..253cfd12 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -207,6 +207,13 @@ function DtRank(DatatypeType) returns (int); // ---------------------------------------------------------------
+// used to make sure function axioms are not used while their consistency is being checked
+const $ModuleContextHeight: int;
+const $FunctionContextHeight: int;
+const $InMethodContext: bool;
+
+// ---------------------------------------------------------------
+
type Field alpha;
type HeapType = <alpha>[ref,Field alpha]alpha;
|