diff options
| author |  leino <unknown> | 2015-04-07 18:20:21 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-07 18:20:21 -0700 |
| commit | 196888695fd805997b02c367d90ac3fbfef32370 (patch) | |
| tree | 13ef4843bafa3785c66e34ee952ee2b2f7ef915e /Test/dafny0/Trait/TraitBasix.dfy.expect | |
| parent | 985579d14df105de939807d1d344fc75ff49563d (diff) | |
Revised look-up and compilation of inherited trait members (static functions/methods don't work yet)
Diffstat (limited to 'Test/dafny0/Trait/TraitBasix.dfy.expect')
| -rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy.expect | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 84465fea..69af0dc5 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,7 +1,7 @@ TraitBasix.dfy(91,24): Error: Undeclared top-level type or type parameter: IX (did you forget to qualify a name?)
-TraitBasix.dfy(77,8): Error: member in the class has been already inherited from its parent trait
-TraitBasix.dfy(70,8): Error: class: I0Child does not implement trait member: Customizable
-TraitBasix.dfy(80,8): Error: class: I0Child2 does not implement trait member: F
-TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor
+TraitBasix.dfy(77,8): Error: field 'x' is inherited from trait 'I2' and is not allowed to be re-declared
+TraitBasix.dfy(70,8): Error: class 'I0Child' does not implement trait method 'I2.Customizable'
+TraitBasix.dfy(80,8): Error: class 'I0Child2' does not implement trait function 'I2.F'
+TraitBasix.dfy(101,15): Error: a trait is not allowed to declare a constructor
TraitBasix.dfy(117,9): Error: new cannot be applied to a trait
6 resolution/type errors detected in TraitBasix.dfy
|