diff options
| author |  Rustan Leino <unknown> | 2014-07-14 19:14:30 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-14 19:14:30 -0700 |
| commit | fda7a92b1f8f2b1fd360aa2b52aa3ddb3c705127 (patch) | |
| tree | 2d9b0bbbfbdd4f73d5d2ba617ce9c78fec8107e0 /Test/dafny0/TypeInstantiations.dfy.expect | |
| parent | 8041bef009e34bb3c5e81ffe7b906ae4347e85d3 (diff) | |
Support for type synonyms in refinements
Started allowing arbitrary types to have type parameters
Diffstat (limited to 'Test/dafny0/TypeInstantiations.dfy.expect')
| -rw-r--r-- | Test/dafny0/TypeInstantiations.dfy.expect | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/TypeInstantiations.dfy.expect b/Test/dafny0/TypeInstantiations.dfy.expect new file mode 100644 index 00000000..6c214970 --- /dev/null +++ b/Test/dafny0/TypeInstantiations.dfy.expect @@ -0,0 +1,13 @@ +TypeInstantiations.dfy(33,7): Error: an arbitrary type declaration (B) in a refining module cannot replace a more specific type declaration in the refinement base
+TypeInstantiations.dfy(36,13): Error: a type declaration that requires equality support cannot be replaced by a codatatype
+TypeInstantiations.dfy(40,7): Error: arbitrary type 'G' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(41,7): Error: arbitrary type 'H' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 2)
+TypeInstantiations.dfy(42,7): Error: arbitrary type 'J' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(51,8): Error: arbitrary type 'R' is not allowed to be replaced by a type that takes a different number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(53,8): Error: arbitrary type 'T' is not allowed to be replaced by a type that takes a different number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(55,7): Error: type 'TP0' is not allowed to change its number of type parameters (got 1, expected 0)
+TypeInstantiations.dfy(56,7): Error: type 'TP1' is not allowed to change its number of type parameters (got 0, expected 1)
+TypeInstantiations.dfy(34,11): Error: type 'C' is used to refine an arbitrary type with equality support, but 'C' does not support equality
+TypeInstantiations.dfy(35,7): Error: type 'D' is used to refine an arbitrary type with equality support, but 'D' does not support equality
+TypeInstantiations.dfy(48,7): Error: type 'N' is used to refine an arbitrary type with equality support, but 'N' does not support equality
+12 resolution/type errors detected in TypeInstantiations.dfy
|