diff options
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);
|