diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 5 | ||||
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 7 |
2 files changed, 0 insertions, 12 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 7c8a9db8..13ea8ed0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -92,11 +92,6 @@ function Set#Disjoint<T>(Set T, Set T): bool; axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
-function Set#Choose<T>(Set T, TickType): T;
-axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
- a != Set#Empty() ==> a[Set#Choose(a, tick)]);
-
-
// ---------------------------------------------------------------
// -- Axiomatization of multisets --------------------------------
// ---------------------------------------------------------------
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 2d17af99..a8faafae 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -162,13 +162,6 @@ namespace Dafny }
return new Set<T>(r);
}
- public T Choose() {
- foreach (T t in dict.Keys) {
- // return the first one
- return t;
- }
- return default(T);
- }
}
public class MultiSet<T>
{
|