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, 7 deletions

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>

   {