3 files changed, 91 insertions, 120 deletions

diff --git a/tests/coq/betree/BetreeMain__Funs.v b/tests/coq/betree/BetreeMain__Funs.v
index a8bb9b74..3ce86f6b 100644
--- a/tests/coq/betree/BetreeMain__Funs.v
+++ b/tests/coq/betree/BetreeMain__Funs.v
@@ -4,11 +4,11 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain__Types .
-Import BetreeMain__Types .
-Require Export BetreeMain__Opaque .
-Import BetreeMain__Opaque .
-Module BetreeMain__Funs .
+Require Export BetreeMain__Types.
+Import BetreeMain__Types.
+Require Export BetreeMain__Opaque.
+Import BetreeMain__Opaque.
+Module BetreeMain__Funs.
 
 (** [betree_main::betree::load_internal_node] *)
 Definition betree_load_internal_node_fwd
@@ -18,7 +18,7 @@ Definition betree_load_internal_node_fwd
   p <- betree_utils_load_internal_node_fwd id st;
   let (st0, l) := p in
   Return (st0, l)
-  .
+.
 
 (** [betree_main::betree::store_internal_node] *)
 Definition betree_store_internal_node_fwd
@@ -28,7 +28,7 @@ Definition betree_store_internal_node_fwd
   p <- betree_utils_store_internal_node_fwd id content st;
   let (st0, _) := p in
   Return (st0, tt)
-  .
+.
 
 (** [betree_main::betree::load_leaf_node] *)
 Definition betree_load_leaf_node_fwd
@@ -36,7 +36,7 @@ Definition betree_load_leaf_node_fwd
   p <- betree_utils_load_leaf_node_fwd id st;
   let (st0, l) := p in
   Return (st0, l)
-  .
+.
 
 (** [betree_main::betree::store_leaf_node] *)
 Definition betree_store_leaf_node_fwd
@@ -46,43 +46,46 @@ Definition betree_store_leaf_node_fwd
   p <- betree_utils_store_leaf_node_fwd id content st;
   let (st0, _) := p in
   Return (st0, tt)
-  .
+.
 
 (** [betree_main::betree::fresh_node_id] *)
 Definition betree_fresh_node_id_fwd (counter : u64) : result u64 :=
-  i <- u64_add counter 1 %u64; let _ := i in Return counter .
+  i <- u64_add counter 1%u64; let _ := i in Return counter
+.
 
 (** [betree_main::betree::fresh_node_id] *)
 Definition betree_fresh_node_id_back (counter : u64) : result u64 :=
-  counter0 <- u64_add counter 1 %u64; Return counter0 .
+  counter0 <- u64_add counter 1%u64; Return counter0
+.
 
 (** [betree_main::betree::NodeIdCounter::{0}::new] *)
 Definition betree_node_id_counter_new_fwd : result Betree_node_id_counter_t :=
-  Return (mkBetree_node_id_counter_t (0 %u64)) .
+  Return (mkBetree_node_id_counter_t (0%u64))
+.
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 Definition betree_node_id_counter_fresh_id_fwd
   (self : Betree_node_id_counter_t) : result u64 :=
   match self with
   | mkBetree_node_id_counter_t id =>
-    i <- u64_add id 1 %u64; let _ := i in Return id
+    i <- u64_add id 1%u64; let _ := i in Return id
   end
-  .
+.
 
 (** [betree_main::betree::NodeIdCounter::{0}::fresh_id] *)
 Definition betree_node_id_counter_fresh_id_back
   (self : Betree_node_id_counter_t) : result Betree_node_id_counter_t :=
   match self with
   | mkBetree_node_id_counter_t id =>
-    i <- u64_add id 1 %u64; Return (mkBetree_node_id_counter_t i)
+    i <- u64_add id 1%u64; Return (mkBetree_node_id_counter_t i)
   end
-  .
+.
 
 (** [core::num::u64::{10}::MAX] *)
 Definition core_num_u64_max_body : result u64 :=
-  Return (18446744073709551615 %u64)
-  .
-Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global .
+  Return (18446744073709551615%u64)
+.
+Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
 
 (** [betree_main::betree::upsert_update] *)
 Definition betree_upsert_update_fwd
@@ -91,7 +94,7 @@ Definition betree_upsert_update_fwd
   | None =>
     match st with
     | BetreeUpsertFunStateAdd v => Return v
-    | BetreeUpsertFunStateSub i => Return (0 %u64)
+    | BetreeUpsertFunStateSub i => Return (0%u64)
     end
   | Some prev0 =>
     match st with
@@ -101,10 +104,10 @@ Definition betree_upsert_update_fwd
       then (i <- u64_add prev0 v; Return i)
       else Return core_num_u64_max_c
     | BetreeUpsertFunStateSub v =>
-      if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0 %u64)
+      if prev0 s>= v then (i <- u64_sub prev0 v; Return i) else Return (0%u64)
     end
   end
-  .
+.
 
 (** [betree_main::betree::List::{1}::len] *)
 Fixpoint betree_list_len_fwd
@@ -114,11 +117,11 @@ Fixpoint betree_list_len_fwd
   | S n0 =>
     match self with
     | BetreeListCons t tl =>
-      i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1 %u64 i; Return i0
-    | BetreeListNil => Return (0 %u64)
+      i <- betree_list_len_fwd T n0 tl; i0 <- u64_add 1%u64 i; Return i0
+    | BetreeListNil => Return (0%u64)
     end
   end
-  .
+.
 
 (** [betree_main::betree::List::{1}::split_at] *)
 Fixpoint betree_list_split_at_fwd
@@ -128,12 +131,12 @@ Fixpoint betree_list_split_at_fwd
   match n with
   | O => Fail_ OutOfFuel
   | S n1 =>
-    if n0 s= 0 %u64
+    if n0 s= 0%u64
     then Return (BetreeListNil, self)
     else
       match self with
       | BetreeListCons hd tl =>
-        i <- u64_sub n0 1 %u64;
+        i <- u64_sub n0 1%u64;
         p <- betree_list_split_at_fwd T n1 tl i;
         let (ls0, ls1) := p in
         let l := ls0 in
@@ -141,7 +144,7 @@ Fixpoint betree_list_split_at_fwd
       | BetreeListNil => Fail_ Failure
       end
   end
-  .
+.
 
 (** [betree_main::betree::List::{1}::push_front] *)
 Definition betree_list_push_front_fwd_back
@@ -149,7 +152,7 @@ Definition betree_list_push_front_fwd_back
   let tl := mem_replace_fwd (Betree_list_t T) self BetreeListNil in
   let l := tl in
   Return (BetreeListCons x l)
-  .
+.
 
 (** [betree_main::betree::List::{1}::pop_front] *)
 Definition betree_list_pop_front_fwd
@@ -159,7 +162,7 @@ Definition betree_list_pop_front_fwd
   | BetreeListCons x tl => Return x
   | BetreeListNil => Fail_ Failure
   end
-  .
+.
 
 (** [betree_main::betree::List::{1}::pop_front] *)
 Definition betree_list_pop_front_back
@@ -169,7 +172,7 @@ Definition betree_list_pop_front_back
   | BetreeListCons x tl => Return tl
   | BetreeListNil => Fail_ Failure
   end
-  .
+.
 
 (** [betree_main::betree::List::{1}::hd] *)
 Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T :=
@@ -177,7 +180,7 @@ Definition betree_list_hd_fwd (T : Type) (self : Betree_list_t T) : result T :=
   | BetreeListCons hd l => Return hd
   | BetreeListNil => Fail_ Failure
   end
-  .
+.
 
 (** [betree_main::betree::List::{2}::head_has_key] *)
 Definition betree_list_head_has_key_fwd
@@ -186,7 +189,7 @@ Definition betree_list_head_has_key_fwd
   | BetreeListCons hd l => let (i, _) := hd in Return (i s= key)
   | BetreeListNil => Return false
   end
-  .
+.
 
 (** [betree_main::betree::List::{2}::partition_at_pivot] *)
 Fixpoint betree_list_partition_at_pivot_fwd
@@ -209,7 +212,7 @@ Fixpoint betree_list_partition_at_pivot_fwd
     | BetreeListNil => Return (BetreeListNil, BetreeListNil)
     end
   end
-  .
+.
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 Definition betree_leaf_split_fwd
@@ -242,7 +245,7 @@ Definition betree_leaf_split_fwd
       end
     end
   end
-  .
+.
 
 (** [betree_main::betree::Leaf::{3}::split] *)
 Definition betree_leaf_split_back
@@ -274,7 +277,7 @@ Definition betree_leaf_split_back
       end
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_in_bindings] *)
 Fixpoint betree_node_lookup_in_bindings_fwd
@@ -296,7 +299,7 @@ Fixpoint betree_node_lookup_in_bindings_fwd
     | BetreeListNil => Return None
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
 Fixpoint betree_node_lookup_first_message_for_key_fwd
@@ -317,7 +320,7 @@ Fixpoint betree_node_lookup_first_message_for_key_fwd
     | BetreeListNil => Return BetreeListNil
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_for_key] *)
 Fixpoint betree_node_lookup_first_message_for_key_back
@@ -340,7 +343,7 @@ Fixpoint betree_node_lookup_first_message_for_key_back
     | BetreeListNil => Return ret
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_upserts] *)
 Fixpoint betree_node_apply_upserts_fwd
@@ -375,7 +378,7 @@ Fixpoint betree_node_apply_upserts_fwd
       let _ := l in
       Return (st0, v))
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_upserts] *)
 Fixpoint betree_node_apply_upserts_back
@@ -408,7 +411,7 @@ Fixpoint betree_node_apply_upserts_back
           BetreeMessageInsert v);
       Return msgs0)
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup] *)
 Fixpoint betree_node_lookup_fwd
@@ -632,7 +635,7 @@ with betree_internal_lookup_in_children_back
         Return (mkBetree_internal_t i i0 n1 n3))
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 Fixpoint betree_node_lookup_mut_in_bindings_fwd
@@ -651,7 +654,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_fwd
     | BetreeListNil => Return BetreeListNil
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_mut_in_bindings] *)
 Fixpoint betree_node_lookup_mut_in_bindings_back
@@ -673,7 +676,7 @@ Fixpoint betree_node_lookup_mut_in_bindings_back
     | BetreeListNil => Return ret
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_to_leaf] *)
 Definition betree_node_apply_to_leaf_fwd_back
@@ -733,7 +736,7 @@ Definition betree_node_apply_to_leaf_fwd_back
         Return bindings2
       end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_leaf] *)
 Fixpoint betree_node_apply_messages_to_leaf_fwd_back
@@ -754,7 +757,7 @@ Fixpoint betree_node_apply_messages_to_leaf_fwd_back
     | BetreeListNil => Return bindings
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::filter_messages_for_key] *)
 Fixpoint betree_node_filter_messages_for_key_fwd_back
@@ -778,7 +781,7 @@ Fixpoint betree_node_filter_messages_for_key_fwd_back
     | BetreeListNil => Return BetreeListNil
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
 Fixpoint betree_node_lookup_first_message_after_key_fwd
@@ -799,7 +802,7 @@ Fixpoint betree_node_lookup_first_message_after_key_fwd
     | BetreeListNil => Return BetreeListNil
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::lookup_first_message_after_key] *)
 Fixpoint betree_node_lookup_first_message_after_key_back
@@ -822,7 +825,7 @@ Fixpoint betree_node_lookup_first_message_after_key_back
     | BetreeListNil => Return ret
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_to_internal] *)
 Definition betree_node_apply_to_internal_fwd_back
@@ -895,7 +898,7 @@ Definition betree_node_apply_to_internal_fwd_back
       msgs2 <- betree_node_lookup_first_message_for_key_back n0 key msgs msgs1;
       Return msgs2)
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_messages_to_internal] *)
 Fixpoint betree_node_apply_messages_to_internal_fwd_back
@@ -916,7 +919,7 @@ Fixpoint betree_node_apply_messages_to_internal_fwd_back
     | BetreeListNil => Return msgs
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply_messages] *)
 Fixpoint betree_node_apply_messages_fwd
@@ -971,7 +974,7 @@ Fixpoint betree_node_apply_messages_fwd
         len <- betree_list_len_fwd (u64 * u64) n0 content0;
         match params with
         | mkBetree_params_t i1 i2 =>
-          i3 <- u64_mul 2 %u64 i2;
+          i3 <- u64_mul 2%u64 i2;
           if len s>= i3
           then (
             p0 <-
@@ -1045,7 +1048,7 @@ with betree_node_apply_messages_back
         len <- betree_list_len_fwd (u64 * u64) n0 content0;
         match params with
         | mkBetree_params_t i1 i2 =>
-          i3 <- u64_mul 2 %u64 i2;
+          i3 <- u64_mul 2%u64 i2;
           if len s>= i3
           then (
             p0 <-
@@ -1168,7 +1171,7 @@ with betree_internal_flush_back
       end
     end
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply] *)
 Definition betree_node_apply_fwd
@@ -1191,7 +1194,7 @@ Definition betree_node_apply_fwd
     let (_, _) := p0 in
     Return (st0, tt)
   end
-  .
+.
 
 (** [betree_main::betree::Node::{5}::apply] *)
 Definition betree_node_apply_back
@@ -1210,7 +1213,7 @@ Definition betree_node_apply_back
     let (self0, node_id_cnt0) := p in
     Return (self0, node_id_cnt0)
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::new] *)
 Definition betree_be_tree_new_fwd
@@ -1223,8 +1226,8 @@ Definition betree_be_tree_new_fwd
   let (st0, _) := p in
   node_id_cnt0 <- betree_node_id_counter_fresh_id_back node_id_cnt;
   Return (st0, mkBetree_be_tree_t (mkBetree_params_t min_flush_size split_size)
-    node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0 %u64))))
-  .
+    node_id_cnt0 (BetreeNodeLeaf (mkBetree_leaf_t id (0%u64))))
+.
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 Definition betree_be_tree_apply_fwd
@@ -1244,7 +1247,7 @@ Definition betree_be_tree_apply_fwd
       Return (st0, tt)
     end
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::apply] *)
 Definition betree_be_tree_apply_back
@@ -1262,7 +1265,7 @@ Definition betree_be_tree_apply_back
       Return (mkBetree_be_tree_t p nic0 n2)
     end
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 Definition betree_be_tree_insert_fwd
@@ -1278,7 +1281,7 @@ Definition betree_be_tree_insert_fwd
     let _ := bt in
     Return (st0, tt)
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::insert] *)
 Definition betree_be_tree_insert_back
@@ -1292,7 +1295,7 @@ Definition betree_be_tree_insert_back
       betree_be_tree_apply_back n0 self key (BetreeMessageInsert value) st;
     Return self0
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
 Definition betree_be_tree_delete_fwd
@@ -1308,7 +1311,7 @@ Definition betree_be_tree_delete_fwd
     let _ := bt in
     Return (st0, tt)
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::delete] *)
 Definition betree_be_tree_delete_back
@@ -1321,7 +1324,7 @@ Definition betree_be_tree_delete_back
     self0 <- betree_be_tree_apply_back n0 self key BetreeMessageDelete st;
     Return self0
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
 Definition betree_be_tree_upsert_fwd
@@ -1338,7 +1341,7 @@ Definition betree_be_tree_upsert_fwd
     let _ := bt in
     Return (st0, tt)
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::upsert] *)
 Definition betree_be_tree_upsert_back
@@ -1353,7 +1356,7 @@ Definition betree_be_tree_upsert_back
       betree_be_tree_apply_back n0 self key (BetreeMessageUpsert upd) st;
     Return self0
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 Definition betree_be_tree_lookup_fwd
@@ -1370,7 +1373,7 @@ Definition betree_be_tree_lookup_fwd
       Return (st0, opt)
     end
   end
-  .
+.
 
 (** [betree_main::betree::BeTree::{6}::lookup] *)
 Definition betree_be_tree_lookup_back
@@ -1386,9 +1389,9 @@ Definition betree_be_tree_lookup_back
       Return (mkBetree_be_tree_t p nic n2)
     end
   end
-  .
+.
 
 (** [betree_main::main] *)
-Definition main_fwd : result unit := Return tt .
+Definition main_fwd : result unit := Return tt.
 
 End BetreeMain__Funs .
diff --git a/tests/coq/betree/BetreeMain__Opaque.v b/tests/coq/betree/BetreeMain__Opaque.v
index 95d4b7c0..cbd8cfb3 100644
--- a/tests/coq/betree/BetreeMain__Opaque.v
+++ b/tests/coq/betree/BetreeMain__Opaque.v
@@ -4,35 +4,35 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Require Export BetreeMain__Types .
-Import BetreeMain__Types .
-Module BetreeMain__Opaque .
+Require Export BetreeMain__Types.
+Import BetreeMain__Types.
+Module BetreeMain__Opaque.
 
 (** [betree_main::betree_utils::load_internal_node] *)
 Axiom betree_utils_load_internal_node_fwd
   : u64 -> state -> result (state * (Betree_list_t (u64 * Betree_message_t)))
-  .
+.
 
 (** [betree_main::betree_utils::store_internal_node] *)
 Axiom betree_utils_store_internal_node_fwd
   :
   u64 -> Betree_list_t (u64 * Betree_message_t) -> state -> result (state *
     unit)
-  .
+.
 
 (** [betree_main::betree_utils::load_leaf_node] *)
 Axiom betree_utils_load_leaf_node_fwd
   : u64 -> state -> result (state * (Betree_list_t (u64 * u64)))
-  .
+.
 
 (** [betree_main::betree_utils::store_leaf_node] *)
 Axiom betree_utils_store_leaf_node_fwd
   : u64 -> Betree_list_t (u64 * u64) -> state -> result (state * unit)
-  .
+.
 
 (** [core::option::Option::{0}::unwrap] *)
 Axiom core_option_option_unwrap_fwd :
-  forall(T : Type) , option T -> state -> result (state * T)
-  .
+  forall(T : Type), option T -> state -> result (state * T)
+.
 
 End BetreeMain__Opaque .
diff --git a/tests/coq/betree/BetreeMain__Types.v b/tests/coq/betree/BetreeMain__Types.v
index 7660a367..2ed0d324 100644
--- a/tests/coq/betree/BetreeMain__Types.v
+++ b/tests/coq/betree/BetreeMain__Types.v
@@ -4,7 +4,7 @@ Require Import Primitives.
 Import Primitives.
 Require Import Coq.ZArith.ZArith.
 Local Open Scope Primitives_scope.
-Module BetreeMain__Types .
+Module BetreeMain__Types.
 
 (** [betree_main::betree::List] *)
 Inductive Betree_list_t (T : Type) :=
@@ -12,8 +12,8 @@ Inductive Betree_list_t (T : Type) :=
 | BetreeListNil : Betree_list_t T
 .
 
-Arguments BetreeListCons {T} _ _  .
-Arguments BetreeListNil {T}  .
+Arguments BetreeListCons {T} _ _.
+Arguments BetreeListNil {T}.
 
 (** [betree_main::betree::UpsertFunState] *)
 Inductive Betree_upsert_fun_state_t :=
@@ -21,9 +21,6 @@ Inductive Betree_upsert_fun_state_t :=
 | BetreeUpsertFunStateSub : u64 -> Betree_upsert_fun_state_t
 .
 
-Arguments BetreeUpsertFunStateAdd _  .
-Arguments BetreeUpsertFunStateSub _  .
-
 (** [betree_main::betree::Message] *)
 Inductive Betree_message_t :=
 | BetreeMessageInsert : u64 -> Betree_message_t
@@ -31,22 +28,13 @@ Inductive Betree_message_t :=
 | BetreeMessageUpsert : Betree_upsert_fun_state_t -> Betree_message_t
 .
 
-Arguments BetreeMessageInsert _  .
-Arguments BetreeMessageDelete  .
-Arguments BetreeMessageUpsert _  .
-
 (** [betree_main::betree::Leaf] *)
 Record Betree_leaf_t :=
-mkBetree_leaf_t
-{
+mkBetree_leaf_t {
   Betree_leaf_id : u64; Betree_leaf_size : u64;
 }
 .
 
-Arguments mkBetree_leaf_t _ _  .
-Arguments Betree_leaf_id  .
-Arguments Betree_leaf_size  .
-
 (** [betree_main::betree::Node] *)
 Inductive Betree_node_t :=
 | BetreeNodeInternal : Betree_internal_t -> Betree_node_t
@@ -62,54 +50,34 @@ with Betree_internal_t :=
   Betree_internal_t
 .
 
-Arguments BetreeNodeInternal _  .
-Arguments BetreeNodeLeaf _  .
-
-Arguments mkBetree_internal_t _ _ _ _  .
-
 (** [betree_main::betree::Params] *)
 Record Betree_params_t :=
-mkBetree_params_t
-{
+mkBetree_params_t {
   Betree_params_min_flush_size : u64; Betree_params_split_size : u64;
 }
 .
 
-Arguments mkBetree_params_t _ _  .
-Arguments Betree_params_min_flush_size  .
-Arguments Betree_params_split_size  .
-
 (** [betree_main::betree::NodeIdCounter] *)
 Record Betree_node_id_counter_t :=
-mkBetree_node_id_counter_t
-{
+mkBetree_node_id_counter_t {
   Betree_node_id_counter_next_node_id : u64;
 }
 .
 
-Arguments mkBetree_node_id_counter_t _  .
-Arguments Betree_node_id_counter_next_node_id  .
-
 (** [betree_main::betree::BeTree] *)
 Record Betree_be_tree_t :=
-mkBetree_be_tree_t
-{
+mkBetree_be_tree_t {
   Betree_be_tree_params : Betree_params_t;
   Betree_be_tree_node_id_cnt : Betree_node_id_counter_t;
   Betree_be_tree_root : Betree_node_t;
 }
 .
 
-Arguments mkBetree_be_tree_t _ _ _  .
-Arguments Betree_be_tree_params  .
-Arguments Betree_be_tree_node_id_cnt  .
-Arguments Betree_be_tree_root  .
-
 (** [core::num::u64::{10}::MAX] *)
 Definition core_num_u64_max_body : result u64 :=
-  Return (18446744073709551615 %u64)
-  .
-Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global .
+  Return (18446744073709551615%u64)
+.
+Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
 
 (** The state type used in the state-error monad *)
 Axiom state : Type.