diff options
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index fa0d1529..9ff60f1b 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -181,6 +181,8 @@ const unique #loc.$Heap: $token; const unique alloc: Field bool;
+function DeclType<T>(Field T) returns (ClassName);
+
function $HeapSucc(HeapType, HeapType) returns (bool);
axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
$HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));
|