From 53281904797b0d78e18a79cc2d140df7ba4b9086 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Sat, 26 Mar 2011 08:54:54 +0000
Subject: Dafny: added "choose" operator on sets

---
 Source/Dafny/DafnyAst.cs | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Source/Dafny/DafnyAst.cs')

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;
-- 
cgit v1.2.3