summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain
diff options
context:
space:
mode:
authorSon Ho2024-03-11 10:20:15 +0100
committerSon Ho2024-03-11 10:20:15 +0100
commit21fdbab049534b35e9573da89bdfd5942144cbb9 (patch)
treedad9a9571e70edf75988a6d3b500e8234a040b3e /tests/lean/BetreeMain
parent82ccc781db0ba1df22f598ad1243fa53dc843320 (diff)
Regenerate the test files
Diffstat (limited to 'tests/lean/BetreeMain')
-rw-r--r--tests/lean/BetreeMain/Funs.lean14
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 96daa197..d6449b37 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -135,7 +135,7 @@ def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
Source: 'src/betree.rs', lines 327:4-327:44 -/
-def betree.ListTupleU64T.head_has_key
+def betree.ListPairU64T.head_has_key
(T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
match self with
| betree.List.Cons hd _ => let (i, _) := hd
@@ -144,7 +144,7 @@ def betree.ListTupleU64T.head_has_key
/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
Source: 'src/betree.rs', lines 339:4-339:73 -/
-divergent def betree.ListTupleU64T.partition_at_pivot
+divergent def betree.ListPairU64T.partition_at_pivot
(T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
:=
@@ -155,7 +155,7 @@ divergent def betree.ListTupleU64T.partition_at_pivot
then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
else
do
- let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
+ let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
let (ls0, ls1) := p
Result.ret (betree.List.Cons (i, t) ls0, ls1)
| betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
@@ -227,7 +227,7 @@ divergent def betree.Node.apply_upserts
Result (State × (U64 × (betree.List (U64 × betree.Message))))
:=
do
- let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
+ let b ← betree.ListPairU64T.head_has_key betree.Message msgs key
if b
then
do
@@ -387,7 +387,7 @@ def betree.Node.apply_to_internal
do
let (msgs1, lookup_first_message_for_key_back) ←
betree.Node.lookup_first_message_for_key key msgs
- let b ← betree.ListTupleU64T.head_has_key betree.Message msgs1 key
+ let b ← betree.ListPairU64T.head_has_key betree.Message msgs1 key
if b
then
match new_msg with
@@ -490,7 +490,7 @@ def betree.Node.apply_to_leaf
do
let (bindings1, lookup_mut_in_bindings_back) ←
betree.Node.lookup_mut_in_bindings key bindings
- let b ← betree.ListTupleU64T.head_has_key U64 bindings1 key
+ let b ← betree.ListPairU64T.head_has_key U64 bindings1 key
if b
then
do
@@ -546,7 +546,7 @@ mutual divergent def betree.Internal.flush
:=
do
let ⟨ i, i1, n, n1 ⟩ := self
- let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i1
+ let p ← betree.ListPairU64T.partition_at_pivot betree.Message content i1
let (msgs_left, msgs_right) := p
let len_left ← betree.List.len (U64 × betree.Message) msgs_left
if len_left >= params.min_flush_size