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 /Source/Dafny/DafnyAst.cs | |
| parent | cd3946b053478afdf7258ce23e34b9ccf51189b5 (diff) | |
Dafny: added "choose" operator on sets
Diffstat (limited to 'Source/Dafny/DafnyAst.cs')
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 0b736242..f5542b4c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2100,6 +2100,7 @@ namespace Microsoft.Dafny { {
public enum Opcode {
Not,
+ SetChoose, // Important: SetChoose is not a function, so it can only be used in a statement context (in particular, the RHS of an assignment)
SeqLength
}
public readonly Opcode Op;
|