diff options
| author |  leino <unknown> | 2014-08-21 14:39:19 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-21 14:39:19 -0700 |
| commit | 81669a1d8bb2e36d86464708bb234e7920776ae6 (patch) | |
| tree | 6de50170760347cf032c864c33992c58cb2905b5 /Test/dafny0/OpaqueFunctionsFail.dfy.expect | |
| parent | a570ecd2d288f67a9e56faf4421a447d06b21d36 (diff) | |
Support for non-constrained derived types ("new types").
Arbitrary conversion from int/real to derived types not yet supported.
Changed rules about numeric type conversions to allow conversions from any numeric type.
Diffstat (limited to 'Test/dafny0/OpaqueFunctionsFail.dfy.expect')
| -rw-r--r-- | Test/dafny0/OpaqueFunctionsFail.dfy.expect | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy.expect b/Test/dafny0/OpaqueFunctionsFail.dfy.expect index 8c2638c3..a893c35e 100644 --- a/Test/dafny0/OpaqueFunctionsFail.dfy.expect +++ b/Test/dafny0/OpaqueFunctionsFail.dfy.expect @@ -1,4 +1,4 @@ -OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called. -OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not determined -OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called. -3 resolution/type errors detected in OpaqueFunctionsFail.dfy +OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not be determined
+OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not be determined. If you are making an opaque function, make sure that the function can be called.
+3 resolution/type errors detected in OpaqueFunctionsFail.dfy
|