summaryrefslogtreecommitdiff
path: root/tests/hashmap
diff options
context:
space:
mode:
authorSon Ho2022-05-15 21:30:49 +0200
committerSon Ho2022-05-15 21:30:49 +0200
commita25d820b6eb02f573ad2c274a35e3496a9dacd40 (patch)
treed491994904b8f57b4b5ed993f61cec2127ebe20c /tests/hashmap
parentf8f07a3135e69529407dfd9359197cb09e78776f (diff)
Treat integer casts in a general manner
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Primitives.fst4
-rw-r--r--tests/hashmap_on_disk/Primitives.fst4
2 files changed, 8 insertions, 0 deletions
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -145,6 +145,10 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x * y)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index 77cf59aa..f73c8c09 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -145,6 +145,10 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
mk_scalar ty (x * y)
+(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+ mk_scalar tgt_ty x
+
/// The scalar types
type isize : eqtype = scalar Isize
type i8 : eqtype = scalar I8