summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
authorSon HO2023-12-05 16:47:51 +0100
committerGitHub2023-12-05 16:47:51 +0100
commit4795e5f823bc89504855d8eb946b111d9314f4d5 (patch)
tree4c35c707e74c14ad7a554147cff20b2e17c28659 /tests/lean/BetreeMain
parent789ba1473acd287814a0d659b5f5a0e480e4e9d7 (diff)
parenta212ab42927e0f9ffa3ed0dfa0140b231e725008 (diff)
Merge pull request #48 from AeneasVerif/son_closures
Prepare support for function pointers and closures
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