From fe11be81341018bf3f3dc73d889f99a6a4b56cdd Mon Sep 17 00:00:00 2001 From: leino Date: Mon, 9 Mar 2015 15:38:38 -0700 Subject: Removed some old and unused functions --- Binaries/DafnyPrelude.bpl | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index f4feacdc..0e91bf95 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -150,22 +150,6 @@ axiom (forall v : T, t : Ty, h : Heap :: { $IsAllocBox($Box(v), t, h) } ( $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v,t,h) )); -// The following functions and axioms are used to obtain a $Box($Unbox(_)) wrapper around -// certain expressions. Note that it assumes any booleans (or, indeed, values of any type) contained -// in the (multi)set are canonical (which is the case for any (multi)set that occurs in an execution of -// a Dafny program). -// The role of the parameter 'dummy' in the following is (an unfortunately clumsy construction -// whose only purpose is) simply to tell Boogie how to instantiate the type parameter 'T'. - -/* -function $IsGoodSet_Extended(s: Set Box, dummy: T): bool; -axiom (forall ss: Set Box, dummy: T, bx: Box :: { $IsGoodSet_Extended(ss, dummy), ss[bx] } - $IsGoodSet_Extended(ss, dummy) ==> ss[bx] ==> bx == $Box($Unbox(bx): T)); -function $IsGoodMultiSet_Extended(ms: MultiSet Box, dummy: T): bool; -axiom (forall ms: MultiSet Box, dummy: T, bx: Box :: { $IsGoodMultiSet_Extended(ms, dummy), ms[bx] } - $IsGoodMultiSet_Extended(ms, dummy) ==> 0 < ms[bx] ==> bx == $Box($Unbox(bx): T)); - */ - // --------------------------------------------------------------- // -- Is and IsAlloc --------------------------------------------- // --------------------------------------------------------------- -- cgit v1.2.3