From a25d820b6eb02f573ad2c274a35e3496a9dacd40 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 15 May 2022 21:30:49 +0200
Subject: Treat integer casts in a general manner

---
 tests/hashmap_on_disk/Primitives.fst | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tests/hashmap_on_disk/Primitives.fst')

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
-- 
cgit v1.2.3