From e5bd97f4ad08b277057a23094f2cc76abbeeaddb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 14 Nov 2022 14:05:26 +0100
Subject: Add a `-use-fuel` option

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

(limited to 'tests/fstar/betree_back_stateful')

diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 82622656..9a06b596 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -45,6 +45,9 @@ let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Re
 type char = FStar.Char.char
 type string = string
 
+let is_zero (n: nat) : bool = n = 0
+let decrease (n: nat{n > 0}) : nat = n - 1
+
 let mem_replace_fwd (a : Type0) (x : a) (y : a) : a = x
 let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
 
-- 
cgit v1.2.3