diff options
| author | Son Ho | 2022-11-09 22:03:04 +0100 |
|---|---|---|
| committer | Son HO | 2022-11-10 11:35:30 +0100 |
| commit | 4ec8646c1bf426c848e8057cdf7c248df6999523 (patch) | |
| tree | 2b5312e198167ef3a1797c1f338bfc511518a106 /tests/hashmap_on_disk | |
| parent | 98ecc4763beb6c6213b26f4ddeb4d7850f8a7c08 (diff) | |
Make a minor cleanup
Diffstat (limited to 'tests/hashmap_on_disk')
| -rw-r--r-- | tests/hashmap_on_disk/Primitives.fst | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst index b44fe9d1..96138e46 100644 --- a/tests/hashmap_on_disk/Primitives.fst +++ b/tests/hashmap_on_disk/Primitives.fst @@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y (*** Scalars *) /// Rk.: most of the following code was at least partially generated -let isize_min : int = -9223372036854775808 -let isize_max : int = 9223372036854775807 +let isize_min : int = -9223372036854775808 // TODO: should be opaque +let isize_max : int = 9223372036854775807 // TODO: should be opaque let i8_min : int = -128 let i8_max : int = 127 let i16_min : int = -32768 @@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807 let i128_min : int = -170141183460469231731687303715884105728 let i128_max : int = 170141183460469231731687303715884105727 let usize_min : int = 0 -let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max] +let usize_max : int = 4294967295 // TODO: should be opaque let u8_min : int = 0 let u8_max : int = 255 let u16_min : int = 0 @@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala mk_scalar ty (x * y) (** Cast an integer from a [src_ty] to a [tgt_ty] *) +// TODO: check the semantics of casts in Rust let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) = mk_scalar tgt_ty x |