diff options
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index cd30fea6..7510363a 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1329,10 +1329,14 @@ Dafny program verifier finished with 12 verified, 0 errors -------------------- EqualityTypes.dfy --------------------
EqualityTypes.dfy(31,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
+EqualityTypes.dfy(32,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(37,11): Error: arbitrary type 'X' is not allowed to be replaced by a datatype that takes type parameters
EqualityTypes.dfy(38,8): Error: arbitrary type 'Y' is not allowed to be replaced by a class that takes type parameters
+EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary type with equality support, but 'X' does not support equality
+EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality
+EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
-4 resolution/type errors detected in EqualityTypes.dfy
+8 resolution/type errors detected in EqualityTypes.dfy
-------------------- SplitExpr.dfy --------------------
|