diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 16 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 10 |
2 files changed, 0 insertions, 26 deletions
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<T> 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<T>(s: Set Box, dummy: T): bool;
-axiom (forall<T> 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<T>(ms: MultiSet Box, dummy: T): bool;
-axiom (forall<T> 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 ---------------------------------------------
// ---------------------------------------------------------------
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a906fb45..ab269ba4 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -11651,7 +11651,6 @@ namespace Microsoft.Dafny { SetEqual,
SetSubset,
SetDisjoint,
- IsGoodSet_Extended,
MultiSetCard,
MultiSetEmpty,
@@ -11665,7 +11664,6 @@ namespace Microsoft.Dafny { MultiSetFromSet,
MultiSetFromSeq,
IsGoodMultiSet,
- IsGoodMultiSet_Extended,
SeqLength,
SeqEmpty,
@@ -11859,10 +11857,6 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args);
- case BuiltinFunction.IsGoodSet_Extended:
- Contract.Assert(args.Length == 2);
- Contract.Assert(typeInstantiation == null);
- return FunctionCall(tok, "$IsGoodSet_Extended", Bpl.Type.Bool, args);
case BuiltinFunction.MultiSetCard:
Contract.Assert(args.Length == 1);
@@ -11914,10 +11908,6 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args);
- case BuiltinFunction.IsGoodMultiSet_Extended:
- Contract.Assert(args.Length == 2);
- Contract.Assert(typeInstantiation == null);
- return FunctionCall(tok, "$IsGoodMultiSet_Extended", Bpl.Type.Bool, args);
case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
|