summaryrefslogtreecommitdiff
path: root/Test/dafny0/ResolutionErrors.dfy.expect
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-06-27 18:56:15 -0700
committerGravatar Rustan Leino <unknown>2014-06-27 18:56:15 -0700
commit05bbbcc402870c5064df987d7f14c5b83cece22c (patch)
tree6de5edc8d615a62951f8d8a7406f11d60b52dad3 /Test/dafny0/ResolutionErrors.dfy.expect
parent16f17e96c48946f925620e1be86fd82cefce923c (diff)
Added tuples and tuple types. Syntax is the expected one, namely parentheses around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy.expect')
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect8
1 files changed, 7 insertions, 1 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 2c0664d9..22f3274e 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -133,4 +133,10 @@ ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only i
ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
-135 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
+141 resolution/type errors detected in ResolutionErrors.dfy