diff options
| author | Guillaume Melquiond | 2020-12-02 06:44:10 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-12-02 07:35:33 +0100 |
| commit | f4dcd1d9f696972e7cbdaa8d70e5abb1a18820ef (patch) | |
| tree | c4503d3a7fbbf5dfcbc5db18c85593e83dd8f6c7 /kernel/uint63_31.ml | |
| parent | 2422d7dee3fda9ac5e65636db937d3d98c85e576 (diff) | |
Make sure the msb is clear.
This is presumably not usable from the surface language. But an ML module
could easily create a proof of false by passing a negative number to
Const.mkInt.
Diffstat (limited to 'kernel/uint63_31.ml')
| -rw-r--r-- | kernel/uint63_31.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 3517f51bfc..988611df3e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -23,9 +23,9 @@ let one = Int64.one (* conversion from an int *) let mask63 i = Int64.logand i maxuint63 -let of_int i = Int64.of_int i +let of_int i = mask63 (Int64.of_int i) let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i) -let of_int64 i = i +let of_int64 = mask63 let to_int64 i = i let to_int_min n m = |