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

---
 tests/lean/BetreeMain/Funs.lean | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 4c862225..0d7cb984 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -256,6 +256,21 @@ divergent def betree.Node.lookup_first_message_for_key_back
         Result.ret (betree.List.Cons (i, m) next_msgs0)
   | betree.List.Nil => Result.ret ret
 
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+   Source: 'src/betree.rs', lines 636:4-636:80 -/
+divergent def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  match bindings with
+  | betree.List.Cons hd tl =>
+    let (i, i0) := hd
+    if i = key
+    then Result.ret (some i0)
+    else
+      if i > key
+      then Result.ret none
+      else betree.Node.lookup_in_bindings key tl
+  | betree.List.Nil => Result.ret none
+
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
    Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts
@@ -316,21 +331,6 @@ divergent def betree.Node.apply_upserts_back
         betree.List.push_front (U64 × betree.Message) msgs (key,
           betree.Message.Insert v)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
-   Source: 'src/betree.rs', lines 636:4-636:80 -/
-divergent def betree.Node.lookup_in_bindings
-  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
-  match bindings with
-  | betree.List.Cons hd tl =>
-    let (i, i0) := hd
-    if i = key
-    then Result.ret (some i0)
-    else
-      if i > key
-      then Result.ret none
-      else betree.Node.lookup_in_bindings key tl
-  | betree.List.Nil => Result.ret none
-
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
    Source: 'src/betree.rs', lines 395:4-395:63 -/
 mutual divergent def betree.Internal.lookup_in_children
-- 
cgit v1.2.3