diff options
Diffstat (limited to 'Test/dafny0/EqualityTypes.dfy')
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy index bbcb988f..251b2e2f 100644 --- a/Test/dafny0/EqualityTypes.dfy +++ b/Test/dafny0/EqualityTypes.dfy @@ -57,11 +57,11 @@ module H { method M<T(==)>(x: T)
{ }
- function F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
{ if x == y then 5 else 7 } // this equality is allowed
- function G<T>(x: Dt<T>, y: Dt<T>): int
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
- function G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
{ if x == y then 5 else 7 } // fine
method Caller0(b: BulkyList, y: int) {
|