diff options
Diffstat (limited to 'Test/dafny0/DerivedTypesResolution.dfy')
| -rw-r--r-- | Test/dafny0/DerivedTypesResolution.dfy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy index c3a02eeb..29f6e859 100644 --- a/Test/dafny0/DerivedTypesResolution.dfy +++ b/Test/dafny0/DerivedTypesResolution.dfy @@ -61,5 +61,8 @@ module Goodies { assert forall ii :: 0 <= ii < |sq| ==> sq[ii] == sq[ii];
var ms := multiset{23.0, 50.0};
assert forall rr :: 0.0 <= rr < 100.0 ==> ms[rr] == ms[rr];
+
+ var truncated := r0.Trunc + x.Trunc;
+ var rounded := (r0 + 0.5).Trunc;
}
}
|