summaryrefslogtreecommitdiff
path: root/tests/coq/betree
diff options
context:
space:
mode:
authorSon Ho2023-11-21 11:50:44 +0100
committerSon Ho2023-11-21 11:50:44 +0100
commit753f7e72f87f5282aee60ad5ada47efeb42625e9 (patch)
tree85805dddd48eacaaac9f482c4c969469e92d73f9 /tests/coq/betree
parent46ab0fc047c69d14e52415bd8b76be167771cd58 (diff)
Regenerate the betree files
Diffstat (limited to 'tests/coq/betree')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v114
-rw-r--r--tests/coq/betree/BetreeMain_Opaque.v2
2 files changed, 58 insertions, 58 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 261e8270..d7428744 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -56,19 +56,19 @@ Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
u64_add counter 1%u64
.
-(** [betree_main::betree::NodeIdCounter::{0}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function *)
Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t :=
Return {| betree_NodeIdCounter_next_node_id := 0%u64 |}
.
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function *)
Definition betree_NodeIdCounter_fresh_id
(self : betree_NodeIdCounter_t) : result u64 :=
_ <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
Return self.(betree_NodeIdCounter_next_node_id)
.
-(** [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 *)
Definition betree_NodeIdCounter_fresh_id_back
(self : betree_NodeIdCounter_t) : result betree_NodeIdCounter_t :=
i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64;
@@ -95,7 +95,7 @@ Definition betree_upsert_update
end
.
-(** [betree_main::betree::List::{1}::len]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function *)
Fixpoint betree_List_len
(T : Type) (n : nat) (self : betree_List_t T) : result u64 :=
match n with
@@ -108,7 +108,7 @@ Fixpoint betree_List_len
end
.
-(** [betree_main::betree::List::{1}::split_at]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function *)
Fixpoint betree_List_split_at
(T : Type) (n : nat) (self : betree_List_t T) (n0 : u64) :
result ((betree_List_t T) * (betree_List_t T))
@@ -131,7 +131,7 @@ Fixpoint betree_List_split_at
end
.
-(** [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Definition betree_List_push_front
(T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) :=
@@ -140,7 +140,7 @@ Definition betree_List_push_front
Return (Betree_List_Cons x l)
.
-(** [betree_main::betree::List::{1}::pop_front]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function *)
Definition betree_List_pop_front
(T : Type) (self : betree_List_t T) : result T :=
let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -150,7 +150,7 @@ Definition betree_List_pop_front
end
.
-(** [betree_main::betree::List::{1}::pop_front]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 *)
Definition betree_List_pop_front_back
(T : Type) (self : betree_List_t T) : result (betree_List_t T) :=
let ls := core_mem_replace (betree_List_t T) self Betree_List_Nil in
@@ -160,7 +160,7 @@ Definition betree_List_pop_front_back
end
.
-(** [betree_main::betree::List::{1}::hd]: forward function *)
+(** [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function *)
Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
match self with
| Betree_List_Cons hd l => Return hd
@@ -168,8 +168,8 @@ Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T :=
end
.
-(** [betree_main::betree::List::{2}::head_has_key]: forward function *)
-Definition betree_List_head_has_key
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function *)
+Definition betree_ListTupleU64T_head_has_key
(T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool :=
match self with
| Betree_List_Cons hd l => let (i, _) := hd in Return (i s= key)
@@ -177,8 +177,8 @@ Definition betree_List_head_has_key
end
.
-(** [betree_main::betree::List::{2}::partition_at_pivot]: forward function *)
-Fixpoint betree_List_partition_at_pivot
+(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function *)
+Fixpoint betree_ListTupleU64T_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)))
:=
@@ -191,7 +191,7 @@ Fixpoint betree_List_partition_at_pivot
if i s>= pivot
then Return (Betree_List_Nil, Betree_List_Cons (i, t) tl)
else (
- p <- betree_List_partition_at_pivot T n0 tl pivot;
+ p <- betree_ListTupleU64T_partition_at_pivot T n0 tl pivot;
let (ls0, ls1) := p in
let l := ls0 in
Return (Betree_List_Cons (i, t) l, ls1))
@@ -200,7 +200,7 @@ Fixpoint betree_List_partition_at_pivot
end
.
-(** [betree_main::betree::Leaf::{3}::split]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function *)
Definition betree_Leaf_split
(n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
(params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -233,7 +233,7 @@ Definition betree_Leaf_split
Return (st1, mkbetree_Internal_t self.(betree_Leaf_id) pivot n0 n1)
.
-(** [betree_main::betree::Leaf::{3}::split]: backward function 2 *)
+(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 *)
Definition betree_Leaf_split_back
(n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64))
(params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t)
@@ -254,7 +254,7 @@ Definition betree_Leaf_split_back
betree_NodeIdCounter_fresh_id_back node_id_cnt0
.
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function *)
Fixpoint betree_Node_lookup_first_message_for_key
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
result (betree_List_t (u64 * betree_Message_t))
@@ -273,7 +273,7 @@ Fixpoint betree_Node_lookup_first_message_for_key
end
.
-(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 *)
Fixpoint betree_Node_lookup_first_message_for_key_back
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
(ret : betree_List_t (u64 * betree_Message_t)) :
@@ -296,7 +296,7 @@ Fixpoint betree_Node_lookup_first_message_for_key_back
end
.
-(** [betree_main::betree::Node::{5}::apply_upserts]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function *)
Fixpoint betree_Node_apply_upserts
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
(key : u64) (st : state) :
@@ -305,7 +305,7 @@ Fixpoint betree_Node_apply_upserts
match n with
| O => Fail_ OutOfFuel
| S n0 =>
- b <- betree_List_head_has_key betree_Message_t msgs key;
+ b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
if b
then (
msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -328,7 +328,7 @@ Fixpoint betree_Node_apply_upserts
end
.
-(** [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 *)
Fixpoint betree_Node_apply_upserts_back
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64)
(key : u64) (st : state) :
@@ -337,7 +337,7 @@ Fixpoint betree_Node_apply_upserts_back
match n with
| O => Fail_ OutOfFuel
| S n0 =>
- b <- betree_List_head_has_key betree_Message_t msgs key;
+ b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs key;
if b
then (
msg <- betree_List_pop_front (u64 * betree_Message_t) msgs;
@@ -358,7 +358,7 @@ Fixpoint betree_Node_apply_upserts_back
end
.
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function *)
Fixpoint betree_Node_lookup_in_bindings
(n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
result (option u64)
@@ -380,7 +380,7 @@ Fixpoint betree_Node_lookup_in_bindings
end
.
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function *)
Fixpoint betree_Internal_lookup_in_children
(n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
result (state * (option u64))
@@ -393,7 +393,7 @@ Fixpoint betree_Internal_lookup_in_children
else betree_Node_lookup n0 self.(betree_Internal_right) key st
end
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 *)
with betree_Internal_lookup_in_children_back
(n : nat) (self : betree_Internal_t) (key : u64) (st : state) :
result betree_Internal_t
@@ -412,7 +412,7 @@ with betree_Internal_lookup_in_children_back
self.(betree_Internal_pivot) self.(betree_Internal_left) n1))
end
-(** [betree_main::betree::Node::{5}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function *)
with betree_Node_lookup
(n : nat) (self : betree_Node_t) (key : u64) (st : state) :
result (state * (option u64))
@@ -483,7 +483,7 @@ with betree_Node_lookup
end
end
-(** [betree_main::betree::Node::{5}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 *)
with betree_Node_lookup_back
(n : nat) (self : betree_Node_t) (key : u64) (st : state) :
result betree_Node_t
@@ -552,7 +552,7 @@ with betree_Node_lookup_back
end
.
-(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Fixpoint betree_Node_filter_messages_for_key
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
@@ -576,7 +576,7 @@ Fixpoint betree_Node_filter_messages_for_key
end
.
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function *)
Fixpoint betree_Node_lookup_first_message_after_key
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
result (betree_List_t (u64 * betree_Message_t))
@@ -595,7 +595,7 @@ Fixpoint betree_Node_lookup_first_message_after_key
end
.
-(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 *)
Fixpoint betree_Node_lookup_first_message_after_key_back
(n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t))
(ret : betree_List_t (u64 * betree_Message_t)) :
@@ -618,7 +618,7 @@ Fixpoint betree_Node_lookup_first_message_after_key_back
end
.
-(** [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Definition betree_Node_apply_to_internal
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64)
@@ -626,7 +626,7 @@ Definition betree_Node_apply_to_internal
result (betree_List_t (u64 * betree_Message_t))
:=
msgs0 <- betree_Node_lookup_first_message_for_key n key msgs;
- b <- betree_List_head_has_key betree_Message_t msgs0 key;
+ b <- betree_ListTupleU64T_head_has_key betree_Message_t msgs0 key;
if b
then
match new_msg with
@@ -676,7 +676,7 @@ Definition betree_Node_apply_to_internal
betree_Node_lookup_first_message_for_key_back n key msgs msgs1)
.
-(** [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Fixpoint betree_Node_apply_messages_to_internal
(n : nat) (msgs : betree_List_t (u64 * betree_Message_t))
@@ -696,7 +696,7 @@ Fixpoint betree_Node_apply_messages_to_internal
end
.
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function *)
Fixpoint betree_Node_lookup_mut_in_bindings
(n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
result (betree_List_t (u64 * u64))
@@ -715,7 +715,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings
end
.
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 *)
Fixpoint betree_Node_lookup_mut_in_bindings_back
(n : nat) (key : u64) (bindings : betree_List_t (u64 * u64))
(ret : betree_List_t (u64 * u64)) :
@@ -737,7 +737,7 @@ Fixpoint betree_Node_lookup_mut_in_bindings_back
end
.
-(** [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Definition betree_Node_apply_to_leaf
(n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64)
@@ -745,7 +745,7 @@ Definition betree_Node_apply_to_leaf
result (betree_List_t (u64 * u64))
:=
bindings0 <- betree_Node_lookup_mut_in_bindings n key bindings;
- b <- betree_List_head_has_key u64 bindings0 key;
+ b <- betree_ListTupleU64T_head_has_key u64 bindings0 key;
if b
then (
hd <- betree_List_pop_front (u64 * u64) bindings0;
@@ -778,7 +778,7 @@ Definition betree_Node_apply_to_leaf
end
.
-(** [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) *)
Fixpoint betree_Node_apply_messages_to_leaf
(n : nat) (bindings : betree_List_t (u64 * u64))
@@ -798,7 +798,7 @@ Fixpoint betree_Node_apply_messages_to_leaf
end
.
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function *)
Fixpoint betree_Internal_flush
(n : nat) (self : betree_Internal_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -809,7 +809,7 @@ Fixpoint betree_Internal_flush
| O => Fail_ OutOfFuel
| S n0 =>
p <-
- betree_List_partition_at_pivot betree_Message_t n0 content
+ betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
self.(betree_Internal_pivot);
let (msgs_left, msgs_right) := p in
len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
@@ -846,7 +846,7 @@ Fixpoint betree_Internal_flush
Return (st0, msgs_left))
end
-(** [betree_main::betree::Internal::{4}::flush]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 *)
with betree_Internal_flush_back
(n : nat) (self : betree_Internal_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -857,7 +857,7 @@ with betree_Internal_flush_back
| O => Fail_ OutOfFuel
| S n0 =>
p <-
- betree_List_partition_at_pivot betree_Message_t n0 content
+ betree_ListTupleU64T_partition_at_pivot betree_Message_t n0 content
self.(betree_Internal_pivot);
let (msgs_left, msgs_right) := p in
len_left <- betree_List_len (u64 * betree_Message_t) n0 msgs_left;
@@ -894,7 +894,7 @@ with betree_Internal_flush_back
node_id_cnt0))
end
-(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function *)
with betree_Node_apply_messages
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -946,7 +946,7 @@ with betree_Node_apply_messages
end
end
-(** [betree_main::betree::Node::{5}::apply_messages]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 *)
with betree_Node_apply_messages_back
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t)
@@ -998,7 +998,7 @@ with betree_Node_apply_messages_back
end
.
-(** [betree_main::betree::Node::{5}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function *)
Definition betree_Node_apply
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1016,7 +1016,7 @@ Definition betree_Node_apply
Return (st0, tt)
.
-(** [betree_main::betree::Node::{5}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 *)
Definition betree_Node_apply_back
(n : nat) (self : betree_Node_t) (params : betree_Params_t)
(node_id_cnt : betree_NodeIdCounter_t) (key : u64)
@@ -1028,7 +1028,7 @@ Definition betree_Node_apply_back
(key, new_msg) l) st
.
-(** [betree_main::betree::BeTree::{6}::new]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function *)
Definition betree_BeTree_new
(min_flush_size : u64) (split_size : u64) (st : state) :
result (state * betree_BeTree_t)
@@ -1052,7 +1052,7 @@ Definition betree_BeTree_new
|})
.
-(** [betree_main::betree::BeTree::{6}::apply]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function *)
Definition betree_BeTree_apply
(n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
(st : state) :
@@ -1068,7 +1068,7 @@ Definition betree_BeTree_apply
Return (st0, tt)
.
-(** [betree_main::betree::BeTree::{6}::apply]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 *)
Definition betree_BeTree_apply_back
(n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t)
(st : state) :
@@ -1086,7 +1086,7 @@ Definition betree_BeTree_apply_back
|}
.
-(** [betree_main::betree::BeTree::{6}::insert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function *)
Definition betree_BeTree_insert
(n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
result (state * unit)
@@ -1097,7 +1097,7 @@ Definition betree_BeTree_insert
Return (st0, tt)
.
-(** [betree_main::betree::BeTree::{6}::insert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 *)
Definition betree_BeTree_insert_back
(n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) :
result betree_BeTree_t
@@ -1105,7 +1105,7 @@ Definition betree_BeTree_insert_back
betree_BeTree_apply_back n self key (Betree_Message_Insert value) st
.
-(** [betree_main::betree::BeTree::{6}::delete]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function *)
Definition betree_BeTree_delete
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result (state * unit)
@@ -1116,7 +1116,7 @@ Definition betree_BeTree_delete
Return (st0, tt)
.
-(** [betree_main::betree::BeTree::{6}::delete]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 *)
Definition betree_BeTree_delete_back
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result betree_BeTree_t
@@ -1124,7 +1124,7 @@ Definition betree_BeTree_delete_back
betree_BeTree_apply_back n self key Betree_Message_Delete st
.
-(** [betree_main::betree::BeTree::{6}::upsert]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function *)
Definition betree_BeTree_upsert
(n : nat) (self : betree_BeTree_t) (key : u64)
(upd : betree_UpsertFunState_t) (st : state) :
@@ -1136,7 +1136,7 @@ Definition betree_BeTree_upsert
Return (st0, tt)
.
-(** [betree_main::betree::BeTree::{6}::upsert]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 *)
Definition betree_BeTree_upsert_back
(n : nat) (self : betree_BeTree_t) (key : u64)
(upd : betree_UpsertFunState_t) (st : state) :
@@ -1145,7 +1145,7 @@ Definition betree_BeTree_upsert_back
betree_BeTree_apply_back n self key (Betree_Message_Upsert upd) st
.
-(** [betree_main::betree::BeTree::{6}::lookup]: forward function *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function *)
Definition betree_BeTree_lookup
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result (state * (option u64))
@@ -1153,7 +1153,7 @@ Definition betree_BeTree_lookup
betree_Node_lookup n self.(betree_BeTree_root) key st
.
-(** [betree_main::betree::BeTree::{6}::lookup]: backward function 0 *)
+(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 *)
Definition betree_BeTree_lookup_back
(n : nat) (self : betree_BeTree_t) (key : u64) (st : state) :
result betree_BeTree_t
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v
index eade90de..bb798e71 100644
--- a/tests/coq/betree/BetreeMain_Opaque.v
+++ b/tests/coq/betree/BetreeMain_Opaque.v
@@ -32,7 +32,7 @@ Axiom betree_utils_store_leaf_node
: u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit)
.
-(** [core::option::Option::{0}::unwrap]: forward function *)
+(** [core::option::{core::option::Option<T>}::unwrap]: forward function *)
Axiom core_option_Option_unwrap :
forall(T : Type), option T -> state -> result (state * T)
.