diff options
| author |  leino <unknown> | 2014-08-02 01:05:17 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-02 01:05:17 -0700 |
| commit | ae578ae92040975fed005d045110679e4e858c31 (patch) | |
| tree | 79f2a3a67c8c9059a89d9771e933c8a0b6b601bf /Test/dafny0/ResolutionErrors.dfy | |
| parent | 54b670417f5974c43ef2fd55d37ba3806ad5c72d (diff) | |
Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in the resolver and translator
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 520b2e38..aaf1291c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1007,20 +1007,20 @@ module CycleError2 { type A = B // error: cycle: A -> B -> A
type B = set<A>
}
-module Good0 {
+module CycleErrors3 {
type A = (B, D<bool>)
type B = C
class C {
var a: A; // this is fine
}
- datatype D<X> = Make(A, B, C) // this is fine, too
+ datatype D<X> = Make(A, B, C) // error: cannot construct a D<X>
}
-module CycleError3 {
+module CycleError4 {
type A = B // error: cycle: A -> B -> A
type B = C<A>
class C<T> { }
}
-module CycleError4 {
+module CycleError5 {
type A = B // error: cycle: A -> B -> A
type B = Dt<A>
datatype Dt<T> = Make(T)
|