diff options
| author |  rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 08:54:54 +0000 |
| commit | d06300cc9bc9f9c7002fb8e555cf172053cdfa5c (patch) | |
| tree | 6c19f930d2b568d7d5128b0642e9d823f6014d6b /Dafny/Compiler.cs | |
| parent | bd9003ec46d72f74c3284a63713336da630769ff (diff) | |
Dafny: added "choose" operator on sets
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index decc5223..bd6f9240 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -1119,6 +1119,10 @@ namespace Microsoft.Dafny { wr.Write("!");
TrParenExpr(e.E);
break;
+ case UnaryExpr.Opcode.SetChoose:
+ TrParenExpr(e.E);
+ wr.Write(".Choose()");
+ break;
case UnaryExpr.Opcode.SeqLength:
if (cce.NonNull(e.E.Type).IsArrayType) {
wr.Write("new BigInteger(");
|