summaryrefslogtreecommitdiff
path: root/tests/coq/betree
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/coq/betree
parent82ccc781db0ba1df22f598ad1243fa53dc843320 (diff)
Regenerate the test files
Diffstat (limited to 'tests/coq/betree')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v14
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index cefab0f4..3863a90f 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -159,7 +159,7 @@ Definition betree_List_hd (T : Type) (self : betree_List_t 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 *)
-Definition betree_ListTupleU64T_head_has_key
+Definition betree_ListPairU64T_head_has_key
(T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
match self with
| Betree_List_Cons hd _ => let (i, _) := hd in Return (i s= key)
@@ -169,7 +169,7 @@ Definition 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 *)
-Fixpoint betree_ListTupleU64T_partition_at_pivot
+Fixpoint betree_ListPairU64T_partition_at_pivot
(T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) :
result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T)))
:=
@@ -182,7 +182,7 @@ Fixpoint betree_ListTupleU64T_partition_at_pivot
if i s>= pivot
then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
else (
- p <- betree_ListTupleU64T_partition_at_pivot T n1 tl pivot;
+ p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot;
let (ls0, ls1) := p in
Return (Betree_List_Cons (i, t) ls0, ls1))
| Betree_List_Nil => Return (Betree_List_Nil, Betree_List_Nil)
@@ -286,7 +286,7 @@ Fixpoint betree_Node_apply_upserts
match n with
| O => Fail_ OutOfFuel
| S n1 =>
- b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
+ b <- betree_ListPairU64T_head_has_key betree_Message_t msgs key;
if b
then (
p <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -462,7 +462,7 @@ Definition betree_Node_apply_to_internal
:=
p <- betree_Node_lookup_first_message_for_key n key msgs;
let (msgs1, lookup_first_message_for_key_back) := p in
- b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs1 key;
+ b <- betree_ListPairU64T_head_has_key betree_Message_t msgs1 key;
if b
then
match new_msg with
@@ -570,7 +570,7 @@ Definition betree_Node_apply_to_leaf
:=
p <- betree_Node_lookup_mut_in_bindings n key bindings;
let (bindings1, lookup_mut_in_bindings_back) := p in
- b <- betree_ListTupleU64T_head_has_key u64 bindings1 key;
+ b <- betree_ListPairU64T_head_has_key u64 bindings1 key;
if b
then (
p1 <- betree_List_pop_front (u64 * u64) bindings1;
@@ -632,7 +632,7 @@ Fixpoint betree_Internal_flush
| O => Fail_ OutOfFuel
| S n1 =>
p <-
- betree_ListTupleU64T_partition_at_pivot betree_Message_t n1 content
+ betree_ListPairU64T_partition_at_pivot betree_Message_t n1 content
self.(betree_Internal_pivot);
let (msgs_left, msgs_right) := p in
len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left;