From 4c1f1d64d5dce2388f7124422e3669cf839fc105 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 16:54:46 +0100
Subject: Regenerate the test files

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

(limited to 'tests/fstar/betree')

diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index dd340c00..a3ffbde4 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -273,6 +273,10 @@ let scalar_shr (#ty0 #ty1 : scalar_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
 
+// This can't fail, but for now we make all casts faillible (easier for the translation)
+let scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) =
+  mk_scalar tgt_ty (if x then 1 else 0)
+
 /// The scalar types
 type isize : eqtype = scalar Isize
 type i8    : eqtype = scalar I8
-- 
cgit v1.2.3