The "choose" statement, hacky and specialized as it was, is now gone. Use the assign-such-that statement instead. For example: x :| x in S;

1 files changed, 0 insertions, 5 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 --------------------------------

 // ---------------------------------------------------------------