summaryrefslogtreecommitdiff
path: root/tests/coq/betree
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v516
-rw-r--r--tests/coq/betree/BetreeMain_Types.v12
2 files changed, 264 insertions, 264 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 85aecfc8..e15085ff 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -260,28 +260,6 @@ Definition betree_leaf_split_back
betree_node_id_counter_fresh_id_back node_id_cnt0
.
-(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_in_bindings_fwd
- (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
- result (option u64)
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s= key
- then Return (Some i0)
- else
- if i s> key
- then Return None
- else betree_node_lookup_in_bindings_fwd n0 key tl
- | BetreeListNil => Return None
- end
- end
-.
-
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function *)
Fixpoint betree_node_lookup_first_message_for_key_fwd
(n : nat) (key : u64) (msgs : Betree_list_t (u64 * Betree_message_t)) :
@@ -386,8 +364,62 @@ Fixpoint betree_node_apply_upserts_back
end
.
+(** [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_in_bindings_fwd
+ (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
+ result (option u64)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s= key
+ then Return (Some i0)
+ else
+ if i s> key
+ then Return None
+ else betree_node_lookup_in_bindings_fwd n0 key tl
+ | BetreeListNil => Return None
+ end
+ end
+.
+
+(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
+Fixpoint betree_internal_lookup_in_children_fwd
+ (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
+ result (state * (option u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if key s< self.(Betree_internal_pivot)
+ then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
+ else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
+ end
+
+(** [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
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ if key s< self.(Betree_internal_pivot)
+ then (
+ n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
+ else (
+ n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
+ end
+
(** [betree_main::betree::Node::{5}::lookup]: forward function *)
-Fixpoint betree_node_lookup_fwd
+with betree_node_lookup_fwd
(n : nat) (self : Betree_node_t) (key : u64) (st : state) :
result (state * (option u64))
:=
@@ -526,144 +558,6 @@ with betree_node_lookup_back
Return (BetreeNodeLeaf node)
end
end
-
-(** [betree_main::betree::Internal::{4}::lookup_in_children]: forward function *)
-with betree_internal_lookup_in_children_fwd
- (n : nat) (self : Betree_internal_t) (key : u64) (st : state) :
- result (state * (option u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- if key s< self.(Betree_internal_pivot)
- then betree_node_lookup_fwd n0 self.(Betree_internal_left) key st
- else betree_node_lookup_fwd n0 self.(Betree_internal_right) key st
- end
-
-(** [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
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- if key s< self.(Betree_internal_pivot)
- then (
- n1 <- betree_node_lookup_back n0 self.(Betree_internal_left) key st;
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 self.(Betree_internal_right)))
- else (
- n1 <- betree_node_lookup_back n0 self.(Betree_internal_right) key st;
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) self.(Betree_internal_left) n1))
- end
-.
-
-(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
-Fixpoint betree_node_lookup_mut_in_bindings_fwd
- (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s>= key
- then Return (BetreeListCons (i, i0) tl)
- else betree_node_lookup_mut_in_bindings_fwd n0 key tl
- | BetreeListNil => Return BetreeListNil
- end
- end
-.
-
-(** [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)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match bindings with
- | BetreeListCons hd tl =>
- let (i, i0) := hd in
- if i s>= key
- then Return ret
- else (
- tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
- Return (BetreeListCons (i, i0) tl0))
- | BetreeListNil => Return ret
- end
- end
-.
-
-(** [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_fwd_back
- (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
- (new_msg : Betree_message_t) :
- result (Betree_list_t (u64 * u64))
- :=
- bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
- b <- betree_list_head_has_key_fwd u64 bindings0 key;
- if b
- then (
- hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
- match new_msg with
- | BetreeMessageInsert v =>
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- bindings2 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2
- | BetreeMessageDelete =>
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- | BetreeMessageUpsert s =>
- let (_, i) := hd in
- v <- betree_upsert_update_fwd (Some i) s;
- bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
- bindings2 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings2
- end)
- else
- match new_msg with
- | BetreeMessageInsert v =>
- bindings1 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- | BetreeMessageDelete =>
- betree_node_lookup_mut_in_bindings_back n key bindings bindings0
- | BetreeMessageUpsert s =>
- v <- betree_upsert_update_fwd None s;
- bindings1 <-
- betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
- betree_node_lookup_mut_in_bindings_back n key bindings bindings1
- end
-.
-
-(** [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_fwd_back
- (n : nat) (bindings : Betree_list_t (u64 * u64))
- (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
- result (Betree_list_t (u64 * u64))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- match new_msgs with
- | BetreeListCons new_msg new_msgs_tl =>
- let (i, m) := new_msg in
- bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
- betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
- | BetreeListNil => Return bindings
- end
- end
.
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
@@ -811,8 +705,210 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
end
.
+(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function *)
+Fixpoint betree_node_lookup_mut_in_bindings_fwd
+ (n : nat) (key : u64) (bindings : Betree_list_t (u64 * u64)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s>= key
+ then Return (BetreeListCons (i, i0) tl)
+ else betree_node_lookup_mut_in_bindings_fwd n0 key tl
+ | BetreeListNil => Return BetreeListNil
+ end
+ end
+.
+
+(** [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)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match bindings with
+ | BetreeListCons hd tl =>
+ let (i, i0) := hd in
+ if i s>= key
+ then Return ret
+ else (
+ tl0 <- betree_node_lookup_mut_in_bindings_back n0 key tl ret;
+ Return (BetreeListCons (i, i0) tl0))
+ | BetreeListNil => Return ret
+ end
+ end
+.
+
+(** [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_fwd_back
+ (n : nat) (bindings : Betree_list_t (u64 * u64)) (key : u64)
+ (new_msg : Betree_message_t) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ bindings0 <- betree_node_lookup_mut_in_bindings_fwd n key bindings;
+ b <- betree_list_head_has_key_fwd u64 bindings0 key;
+ if b
+ then (
+ hd <- betree_list_pop_front_fwd (u64 * u64) bindings0;
+ match new_msg with
+ | BetreeMessageInsert v =>
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ bindings2 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+ | BetreeMessageDelete =>
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ | BetreeMessageUpsert s =>
+ let (_, i) := hd in
+ v <- betree_upsert_update_fwd (Some i) s;
+ bindings1 <- betree_list_pop_front_back (u64 * u64) bindings0;
+ bindings2 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings1 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings2
+ end)
+ else
+ match new_msg with
+ | BetreeMessageInsert v =>
+ bindings1 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ | BetreeMessageDelete =>
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings0
+ | BetreeMessageUpsert s =>
+ v <- betree_upsert_update_fwd None s;
+ bindings1 <-
+ betree_list_push_front_fwd_back (u64 * u64) bindings0 (key, v);
+ betree_node_lookup_mut_in_bindings_back n key bindings bindings1
+ end
+.
+
+(** [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_fwd_back
+ (n : nat) (bindings : Betree_list_t (u64 * u64))
+ (new_msgs : Betree_list_t (u64 * Betree_message_t)) :
+ result (Betree_list_t (u64 * u64))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ match new_msgs with
+ | BetreeListCons new_msg new_msgs_tl =>
+ let (i, m) := new_msg in
+ bindings0 <- betree_node_apply_to_leaf_fwd_back n0 bindings i m;
+ betree_node_apply_messages_to_leaf_fwd_back n0 bindings0 new_msgs_tl
+ | BetreeListNil => Return bindings
+ end
+ end
+.
+
+(** [betree_main::betree::Internal::{4}::flush]: forward function *)
+Fixpoint betree_internal_flush_fwd
+ (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
+ (node_id_cnt : Betree_node_id_counter_t)
+ (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
+ result (state * (Betree_list_t (u64 * Betree_message_t)))
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ p <-
+ betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+ self.(Betree_internal_pivot);
+ let (msgs_left, msgs_right) := p in
+ len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+ if len_left s>= params.(Betree_params_min_flush_size)
+ then (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (st0, _) := p0 in
+ p1 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (_, node_id_cnt0) := p1 in
+ len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+ if len_right s>= params.(Betree_params_min_flush_size)
+ then (
+ p2 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+ node_id_cnt0 msgs_right st0;
+ let (st1, _) := p2 in
+ _ <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right)
+ params node_id_cnt0 msgs_right st0;
+ Return (st1, BetreeListNil))
+ else Return (st0, msgs_right))
+ else (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ let (st0, _) := p0 in
+ _ <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ Return (st0, msgs_left))
+ end
+
+(** [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_node_id_counter_t)
+ (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
+ result (Betree_internal_t * Betree_node_id_counter_t)
+ :=
+ match n with
+ | O => Fail_ OutOfFuel
+ | S n0 =>
+ p <-
+ betree_list_partition_at_pivot_fwd Betree_message_t n0 content
+ self.(Betree_internal_pivot);
+ let (msgs_left, msgs_right) := p in
+ len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
+ if len_left s>= params.(Betree_params_min_flush_size)
+ then (
+ p0 <-
+ betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (st0, _) := p0 in
+ p1 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_left) params
+ node_id_cnt msgs_left st;
+ let (n1, node_id_cnt0) := p1 in
+ len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
+ if len_right s>= params.(Betree_params_min_flush_size)
+ then (
+ p2 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right)
+ params node_id_cnt0 msgs_right st0;
+ let (n2, node_id_cnt1) := p2 in
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
+ else
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
+ node_id_cnt0))
+ else (
+ p0 <-
+ betree_node_apply_messages_back n0 self.(Betree_internal_right) params
+ node_id_cnt msgs_right st;
+ let (n1, node_id_cnt0) := p0 in
+ Return (mkBetree_internal_t self.(Betree_internal_id)
+ self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
+ node_id_cnt0))
+ end
+
(** [betree_main::betree::Node::{5}::apply_messages]: forward function *)
-Fixpoint betree_node_apply_messages_fwd
+with betree_node_apply_messages_fwd
(n : nat) (self : Betree_node_t) (params : Betree_params_t)
(node_id_cnt : Betree_node_id_counter_t)
(msgs : Betree_list_t (u64 * Betree_message_t)) (st : state) :
@@ -922,102 +1018,6 @@ with betree_node_apply_messages_back
|}, node_id_cnt))
end
end
-
-(** [betree_main::betree::Internal::{4}::flush]: forward function *)
-with betree_internal_flush_fwd
- (n : nat) (self : Betree_internal_t) (params : Betree_params_t)
- (node_id_cnt : Betree_node_id_counter_t)
- (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
- result (state * (Betree_list_t (u64 * Betree_message_t)))
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- p <-
- betree_list_partition_at_pivot_fwd Betree_message_t n0 content
- self.(Betree_internal_pivot);
- let (msgs_left, msgs_right) := p in
- len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
- if len_left s>= params.(Betree_params_min_flush_size)
- then (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (st0, _) := p0 in
- p1 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (_, node_id_cnt0) := p1 in
- len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
- if len_right s>= params.(Betree_params_min_flush_size)
- then (
- p2 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
- node_id_cnt0 msgs_right st0;
- let (st1, _) := p2 in
- _ <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right)
- params node_id_cnt0 msgs_right st0;
- Return (st1, BetreeListNil))
- else Return (st0, msgs_right))
- else (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- let (st0, _) := p0 in
- _ <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- Return (st0, msgs_left))
- end
-
-(** [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_node_id_counter_t)
- (content : Betree_list_t (u64 * Betree_message_t)) (st : state) :
- result (Betree_internal_t * Betree_node_id_counter_t)
- :=
- match n with
- | O => Fail_ OutOfFuel
- | S n0 =>
- p <-
- betree_list_partition_at_pivot_fwd Betree_message_t n0 content
- self.(Betree_internal_pivot);
- let (msgs_left, msgs_right) := p in
- len_left <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_left;
- if len_left s>= params.(Betree_params_min_flush_size)
- then (
- p0 <-
- betree_node_apply_messages_fwd n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (st0, _) := p0 in
- p1 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_left) params
- node_id_cnt msgs_left st;
- let (n1, node_id_cnt0) := p1 in
- len_right <- betree_list_len_fwd (u64 * Betree_message_t) n0 msgs_right;
- if len_right s>= params.(Betree_params_min_flush_size)
- then (
- p2 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right)
- params node_id_cnt0 msgs_right st0;
- let (n2, node_id_cnt1) := p2 in
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 n2, node_id_cnt1))
- else
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) n1 self.(Betree_internal_right),
- node_id_cnt0))
- else (
- p0 <-
- betree_node_apply_messages_back n0 self.(Betree_internal_right) params
- node_id_cnt msgs_right st;
- let (n1, node_id_cnt0) := p0 in
- Return (mkBetree_internal_t self.(Betree_internal_id)
- self.(Betree_internal_pivot) self.(Betree_internal_left) n1,
- node_id_cnt0))
- end
.
(** [betree_main::betree::Node::{5}::apply]: forward function *)
diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v
index c8af54cd..4a4e75aa 100644
--- a/tests/coq/betree/BetreeMain_Types.v
+++ b/tests/coq/betree/BetreeMain_Types.v
@@ -37,19 +37,19 @@ mkBetree_leaf_t {
}
.
-(** [betree_main::betree::Node] *)
-Inductive Betree_node_t :=
-| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
-| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
-
(** [betree_main::betree::Internal] *)
-with Betree_internal_t :=
+Inductive Betree_internal_t :=
| mkBetree_internal_t :
u64 ->
u64 ->
Betree_node_t ->
Betree_node_t ->
Betree_internal_t
+
+(** [betree_main::betree::Node] *)
+with Betree_node_t :=
+| BetreeNodeInternal : Betree_internal_t -> Betree_node_t
+| BetreeNodeLeaf : Betree_leaf_t -> Betree_node_t
.
Definition Betree_internal_id (x : Betree_internal_t) :=