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/coq/betree/Primitives.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tests/coq/betree')

diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 99ffe070..84280b96 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -266,6 +266,10 @@ Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty
 Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) :=
   mk_scalar tgt_ty (to_Z x).
 
+(* This can't fail, but for now we make all casts faillible (easier for the translation) *)
+Definition scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) :=
+  mk_scalar tgt_ty (if x then 1 else 0).
+
 (** Comparisons *)
 Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool :=
   Z.leb (to_Z x) (to_Z y) .
-- 
cgit v1.2.3