diff options
| author | Son Ho | 2023-12-05 15:00:46 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 15:00:46 +0100 |
| commit | 60ce69b83cbd749781543bb16becb5357f0e1a0a (patch) | |
| tree | bd847cb3ed7a00644ea643325468e5328f06e220 /tests/lean/BetreeMain | |
| parent | 054d7256ed90f752ae6b39ebba608f89076d38e7 (diff) | |
Update following changes in Charon
Diffstat (limited to 'tests/lean/BetreeMain')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 30 |
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 |