From 60ce69b83cbd749781543bb16becb5357f0e1a0a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 5 Dec 2023 15:00:46 +0100
Subject: Update following changes in Charon

---
 .../fstar/betree_back_stateful/BetreeMain.Funs.fst | 32 +++++++++++-----------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'tests/fstar/betree_back_stateful/BetreeMain.Funs.fst')

diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index b912a316..6c3c2161 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -295,6 +295,22 @@ let rec betree_Node_lookup_first_message_for_key_back
   | Betree_List_Nil -> Return ret
   end
 
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+    Source: 'src/betree.rs', lines 636:4-636:80 *)
+let rec betree_Node_lookup_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
+  =
+  begin match bindings with
+  | Betree_List_Cons hd tl ->
+    let (i, i0) = hd in
+    if i = key
+    then Return (Some i0)
+    else if i > key then Return None else betree_Node_lookup_in_bindings key tl
+  | Betree_List_Nil -> Return None
+  end
+
 (** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
     Source: 'src/betree.rs', lines 819:4-819:90 *)
 let rec betree_Node_apply_upserts
@@ -351,22 +367,6 @@ let rec betree_Node_apply_upserts_back
         Betree_Message_Insert v) in
     Return (st0, msgs0)
 
-(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
-    Source: 'src/betree.rs', lines 636:4-636:80 *)
-let rec betree_Node_lookup_in_bindings
-  (key : u64) (bindings : betree_List_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_Node_lookup_in_bindings_decreases key bindings))
-  =
-  begin match bindings with
-  | Betree_List_Cons hd tl ->
-    let (i, i0) = hd in
-    if i = key
-    then Return (Some i0)
-    else if i > key then Return None else betree_Node_lookup_in_bindings key tl
-  | Betree_List_Nil -> Return None
-  end
-
 (** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
     Source: 'src/betree.rs', lines 395:4-395:63 *)
 let rec betree_Internal_lookup_in_children
-- 
cgit v1.2.3