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/ResolutionErrors.dfy | |
| 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/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 3c9156dd..38f2f9c2 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -957,9 +957,9 @@ method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real s := (2.0 / 1.7) + (r / s) - (--r) * -12.3;
- s := real(s); // error: cannot convert real->real
- j := int(j); // error: cannot convert int->int
- j := int(n); // error: cannot convert nat->int
+ s := real(s); // fine (identity transform)
+ j := int(j); // fine (identity transform)
+ j := int(n); // fine (identity transform)
}
// --- filling in type arguments and checking that there aren't too many ---
|