diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 1069f419..d4c97f0f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -646,6 +646,9 @@ axiom (forall b: BoxType, h: HeapType, t: BoxType :: axiom (forall b: BoxType, h: HeapType ::
{ GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }
GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));
+axiom (forall dt: DatatypeType, h: HeapType ::
+ { GenericAlloc($Box(dt), h) }
+ GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h));
// ==> GenericAlloc
axiom (forall b: bool, h: HeapType ::
$IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
|