summaryrefslogtreecommitdiff
path: root/Test/dafny0/EqualityTypes.dfy.expect
blob: 410e4507f267ad1c533f2ffd485b1825c115b4ab (plain)
1
2
3
4
5
6
7
8
9
10
11
12
EqualityTypes.dfy(34,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
EqualityTypes.dfy(35,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(40,11): Error: opaque type 'X' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
EqualityTypes.dfy(41,8): Error: opaque type 'Y' is not allowed to be replaced by a class that takes a different number of type parameters (got 1, expected 0)
EqualityTypes.dfy(45,11): Error: type 'X' is used to refine an opaque type with equality support, but 'X' does not support equality
EqualityTypes.dfy(46,11): Error: type 'Y' is used to refine an opaque type with equality support, but 'Y' does not support equality
EqualityTypes.dfy(66,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)
EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)
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