diff options
| author |  rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
| commit | 53281904797b0d78e18a79cc2d140df7ba4b9086 (patch) | |
| tree | 6f1b098b301fc8e6594c22199fb94a257164b7d5 /Binaries/DafnyRuntime.cs | |
| parent | cd3946b053478afdf7258ce23e34b9ccf51189b5 (diff) | |
Dafny: added "choose" operator on sets
Diffstat (limited to 'Binaries/DafnyRuntime.cs')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index f32cc85a..63cca64a 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -117,6 +117,12 @@ namespace Dafny }
return new Set<T>(r);
}
+ public T Choose() {
+ foreach (T t in dict.Keys) {
+ // return the first one
+ return t;
+ }
+ }
}
public class Sequence<T>
{
|