diff options
| author |  leino <unknown> | 2014-08-13 00:42:08 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-13 00:42:08 -0700 |
| commit | 7456be76add1e5d52001657df80d0e3cb00d5065 (patch) | |
| tree | 7caf54a9a4409ca3e6cc766e7699075b828ecb9f /Test/dafny0/EqualityTypes.dfy.expect | |
| parent | 08ab990d6f1a188c6cc039d6a2289daf41ff52d3 (diff) | |
Check for proper use of equality-supporting types also in local variables and forall statements, and more expressions
Diffstat (limited to 'Test/dafny0/EqualityTypes.dfy.expect')
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy.expect | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index 70e46ff0..f296ed4b 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -9,4 +9,30 @@ EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must sup EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)
-11 resolution/type errors detected in EqualityTypes.dfy
+EqualityTypes.dfy(147,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(149,13): Error: type parameter 0 (Y) passed to function G must support equality (got Co)
+EqualityTypes.dfy(156,11): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(173,8): Error: set argument type must support equality (got Dt<Co>)
+EqualityTypes.dfy(176,8): Error: set argument type must support equality (got Left<Co,int>)
+EqualityTypes.dfy(177,8): Error: type parameter 1 (U) passed to type Right must support equality (got Co)
+EqualityTypes.dfy(179,8): Error: type parameter 1 (U) passed to type RightExplicit must support equality (got Co)
+EqualityTypes.dfy(181,8): Error: set argument type must support equality (got Syn<int,int,Co>)
+EqualityTypes.dfy(184,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(185,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(192,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(196,11): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(196,20): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
+EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
+EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)
+EqualityTypes.dfy(241,8): Error: map domain type must support equality (got Co)
+EqualityTypes.dfy(241,14): Error: map domain type must support equality (got Co)
+37 resolution/type errors detected in EqualityTypes.dfy
|