diff options
| author | Son HO | 2023-12-05 16:47:51 +0100 |
|---|---|---|
| committer | GitHub | 2023-12-05 16:47:51 +0100 |
| commit | 4795e5f823bc89504855d8eb946b111d9314f4d5 (patch) | |
| tree | 4c35c707e74c14ad7a554147cff20b2e17c28659 /tests/lean/BetreeMain/Funs.lean | |
| parent | 789ba1473acd287814a0d659b5f5a0e480e4e9d7 (diff) | |
| parent | a212ab42927e0f9ffa3ed0dfa0140b231e725008 (diff) | |
Merge pull request #48 from AeneasVerif/son_closures
Prepare support for function pointers and closures
Diffstat (limited to 'tests/lean/BetreeMain/Funs.lean')
| -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 |