diff options
author | 2013-03-27 13:51:16 -0700 | |
---|---|---|
committer | 2013-03-27 13:51:16 -0700 | |
commit | 5296b17758c3e27bf551e9a322323a37983d7abb (patch) | |
tree | a7c818eedf1608eec0e59ff73ac3ee8356939751 /Source/Dafny/Resolver.cs | |
parent | 5f05e3a1c194dcda48115d7b6a1c5777bd2d5287 (diff) |
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;
Diffstat (limited to 'Source/Dafny/Resolver.cs')
-rw-r--r-- | Source/Dafny/Resolver.cs | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c70c039d..bab0aca7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4472,11 +4472,6 @@ namespace Microsoft.Dafny } else {
Error(rhs.Tok, "new allocation not allowed in ghost context");
}
- } else if (rhs is ExprRhs) {
- var r = ((ExprRhs)rhs).Expr.Resolved;
- if (kind == ForallStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
- Error(r, "set choose operator not supported inside the enclosing forall statement");
- }
}
} else if (stmt is VarDecl) {
// cool
@@ -5234,13 +5229,6 @@ namespace Microsoft.Dafny }
expr.Type = Type.Bool;
break;
- case UnaryExpr.Opcode.SetChoose:
- var elType = new InferredTypeProxy();
- if (!UnifyTypes(e.E.Type, new SetType(elType))) {
- Error(expr, "choose operator expects a set argument (instead got {0})", e.E.Type);
- }
- expr.Type = elType;
- break;
case UnaryExpr.Opcode.SeqLength:
if (!UnifyTypes(e.E.Type, new CollectionTypeProxy(new InferredTypeProxy()))) {
Error(expr, "size operator expects a collection argument (instead got {0})", e.E.Type);
|