summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
authorSon Ho2023-12-05 15:00:46 +0100
committerSon Ho2023-12-05 15:00:46 +0100
commit60ce69b83cbd749781543bb16becb5357f0e1a0a (patch)
treebd847cb3ed7a00644ea643325468e5328f06e220 /tests/lean/BetreeMain
parent054d7256ed90f752ae6b39ebba608f89076d38e7 (diff)
Update following changes in Charon
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Funs.lean30
1 files changed, 15 insertions, 15 deletions
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