Merge branch 'main' into son/loops2

7 files changed, 123 insertions, 121 deletions

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/Betree/Funs.lean
index 7cc52159..8612ccbc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -1,13 +1,13 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: function definitions
+-- [betree]: function definitions
 import Base
-import BetreeMain.Types
-import BetreeMain.FunsExternal
+import Betree.Types
+import Betree.FunsExternal
 open Primitives
 
-namespace betree_main
+namespace betree
 
-/- [betree_main::betree::load_internal_node]:
+/- [betree::betree::load_internal_node]:
    Source: 'src/betree.rs', lines 36:0-36:52 -/
 def betree.load_internal_node
   (id : U64) (st : State) :
@@ -15,7 +15,7 @@ def betree.load_internal_node
   :=
   betree_utils.load_internal_node id st
 
-/- [betree_main::betree::store_internal_node]:
+/- [betree::betree::store_internal_node]:
    Source: 'src/betree.rs', lines 41:0-41:60 -/
 def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
@@ -23,13 +23,13 @@ def betree.store_internal_node
   :=
   betree_utils.store_internal_node id content st
 
-/- [betree_main::betree::load_leaf_node]:
+/- [betree::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
 def betree.load_leaf_node
   (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) :=
   betree_utils.load_leaf_node id st
 
-/- [betree_main::betree::store_leaf_node]:
+/- [betree::betree::store_leaf_node]:
    Source: 'src/betree.rs', lines 51:0-51:52 -/
 def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
@@ -37,19 +37,19 @@ def betree.store_leaf_node
   :=
   betree_utils.store_leaf_node id content st
 
-/- [betree_main::betree::fresh_node_id]:
+/- [betree::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
 def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
   let counter1 ← counter + 1#u64
   Result.ok (counter, counter1)
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
+/- [betree::betree::{betree::betree::NodeIdCounter}::new]:
    Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ok { next_node_id := 0#u64 }
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
+/- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]:
    Source: 'src/betree.rs', lines 210:4-210:36 -/
 def betree.NodeIdCounter.fresh_id
   (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
@@ -57,7 +57,7 @@ def betree.NodeIdCounter.fresh_id
   let i ← self.next_node_id + 1#u64
   Result.ok (self.next_node_id, { next_node_id := i })
 
-/- [betree_main::betree::upsert_update]:
+/- [betree::betree::upsert_update]:
    Source: 'src/betree.rs', lines 234:0-234:70 -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -79,7 +79,7 @@ def betree.upsert_update
       then prev1 - v
       else Result.ok 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
+/- [betree::betree::{betree::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
@@ -88,7 +88,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
                              1#u64 + i
   | betree.List.Nil => Result.ok 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
    Source: 'src/betree.rs', lines 284:4-284:51 -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
@@ -106,14 +106,14 @@ divergent def betree.List.split_at
       Result.ok (betree.List.Cons hd ls0, ls1)
     | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
+/- [betree::betree::{betree::betree::List<T>#1}::push_front]:
    Source: 'src/betree.rs', lines 299:4-299:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
   Result.ok (betree.List.Cons x tl)
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
+/- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 306:4-306:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
@@ -122,14 +122,14 @@ def betree.List.pop_front
   | betree.List.Cons x tl => Result.ok (x, tl)
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
+/- [betree::betree::{betree::betree::List<T>#1}::hd]:
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
    Source: 'src/betree.rs', lines 327:4-327:44 -/
 def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
@@ -138,7 +138,7 @@ def betree.ListPairU64T.head_has_key
                              Result.ok (i = key)
   | betree.List.Nil => Result.ok false
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
 divergent def betree.ListPairU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
@@ -156,7 +156,7 @@ divergent def betree.ListPairU64T.partition_at_pivot
       Result.ok (betree.List.Cons (i, t) ls0, ls1)
   | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
+/- [betree::betree::{betree::betree::Leaf#3}::split]:
    Source: 'src/betree.rs', lines 359:4-364:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
@@ -176,7 +176,7 @@ def betree.Leaf.split
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
   Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -200,7 +200,7 @@ divergent def betree.Node.lookup_first_message_for_key
       Result.ok (l, back)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 636:4-636:80 -/
 divergent def betree.Node.lookup_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
@@ -215,7 +215,7 @@ divergent def betree.Node.lookup_in_bindings
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ok none
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
@@ -244,24 +244,23 @@ divergent def betree.Node.apply_upserts
         betree.Message.Insert v)
     Result.ok (v, msgs1)
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
+/- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
   :=
-  let ⟨ i, i1, n, n1 ⟩ := self
-  if key < i1
+  if key < self.pivot
   then
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
+    let (st1, (o, n)) ← betree.Node.lookup self.left key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right))
   else
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n1 key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
+    let (st1, (o, n)) ← betree.Node.lookup self.right key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
+/- [betree::betree::{betree::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
@@ -270,8 +269,7 @@ divergent def betree.Node.lookup
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, msgs) ← betree.load_internal_node i st
+    let (st1, msgs) ← betree.load_internal_node node.id st
     let (pending, lookup_first_message_for_key_back) ←
       betree.Node.lookup_first_message_for_key key msgs
     match pending with
@@ -281,8 +279,7 @@ divergent def betree.Node.lookup
       then
         do
         let (st2, (o, node1)) ←
-          betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-            st1
+          betree.Internal.lookup_in_children node key st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
         Result.ok (st2, (o, betree.Node.Internal node1))
@@ -293,33 +290,26 @@ divergent def betree.Node.lookup
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Insert v) l)
-          Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
-            i1 n n1)))
+          Result.ok (st1, (some v, betree.Node.Internal node))
         | betree.Message.Delete =>
           do
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Delete) l)
-          Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
-            n n1)))
+          Result.ok (st1, (none, betree.Node.Internal node))
         | betree.Message.Upsert ufs =>
           do
           let (st2, (v, node1)) ←
-            betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
-              key st1
+            betree.Internal.lookup_in_children node key st1
           let (v1, pending1) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
               betree.Message.Upsert ufs) l) v key
-          let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
-          let (st3, _) ← betree.store_internal_node i2 msgs1 st2
-          Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2
-            i3 n2 n3)))
+          let (st3, _) ← betree.store_internal_node node1.id msgs1 st2
+          Result.ok (st3, (some v1, betree.Node.Internal node1))
     | betree.List.Nil =>
       do
-      let (st2, (o, node1)) ←
-        betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-          st1
+      let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
       Result.ok (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
@@ -330,7 +320,7 @@ divergent def betree.Node.lookup
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
    Source: 'src/betree.rs', lines 674:4-674:77 -/
 divergent def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -349,7 +339,7 @@ divergent def betree.Node.filter_messages_for_key
     else Result.ok (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ok betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -373,7 +363,7 @@ divergent def betree.Node.lookup_first_message_after_key
     else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
+/- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
    Source: 'src/betree.rs', lines 521:4-521:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
@@ -437,7 +427,7 @@ def betree.Node.apply_to_internal
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
     lookup_first_message_for_key_back msgs2
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 502:4-505:5 -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
@@ -452,7 +442,7 @@ divergent def betree.Node.apply_messages_to_internal
     betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
   | betree.List.Nil => Result.ok msgs
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) :
@@ -476,7 +466,7 @@ divergent def betree.Node.lookup_mut_in_bindings
       Result.ok (l, back)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
+/- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
    Source: 'src/betree.rs', lines 460:4-460:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
@@ -516,7 +506,7 @@ def betree.Node.apply_to_leaf
       let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
       lookup_mut_in_bindings_back bindings2
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 444:4-447:5 -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
@@ -531,7 +521,7 @@ divergent def betree.Node.apply_messages_to_leaf
     betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
   | betree.List.Nil => Result.ok bindings
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
+/- [betree::betree::{betree::betree::Internal#4}::flush]:
    Source: 'src/betree.rs', lines 410:4-415:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
@@ -541,36 +531,38 @@ mutual divergent def betree.Internal.flush
     × betree.NodeIdCounter)))
   :=
   do
-  let ⟨ i, i1, n, n1 ⟩ := self
-  let p ← betree.ListPairU64T.partition_at_pivot betree.Message content i1
+  let p ←
+    betree.ListPairU64T.partition_at_pivot betree.Message content self.pivot
   let (msgs_left, msgs_right) := p
   let len_left ← betree.List.len (U64 × betree.Message) msgs_left
   if len_left >= params.min_flush_size
   then
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n params node_id_cnt msgs_left st
-    let (n2, node_id_cnt1) := p1
+      betree.Node.apply_messages self.left params node_id_cnt msgs_left st
+    let (n, node_id_cnt1) := p1
     let len_right ← betree.List.len (U64 × betree.Message) msgs_right
     if len_right >= params.min_flush_size
     then
       do
       let (st2, p2) ←
-        betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
-      let (n3, node_id_cnt2) := p2
-      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
-        node_id_cnt2)))
+        betree.Node.apply_messages self.right params node_id_cnt1 msgs_right
+          st1
+      let (n1, node_id_cnt2) := p2
+      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot
+        n n1, node_id_cnt2)))
     else
-      Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
-        node_id_cnt1)))
+      Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n
+        self.right, node_id_cnt1)))
   else
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n1 params node_id_cnt msgs_right st
-    let (n2, node_id_cnt1) := p1
-    Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+      betree.Node.apply_messages self.right params node_id_cnt msgs_right st
+    let (n, node_id_cnt1) := p1
+    Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot
+      self.left n, node_id_cnt1)))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
@@ -581,26 +573,21 @@ divergent def betree.Node.apply_messages
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, content) ← betree.load_internal_node i st
+    let (st1, content) ← betree.load_internal_node node.id st
     let content1 ← betree.Node.apply_messages_to_internal content msgs
     let num_msgs ← betree.List.len (U64 × betree.Message) content1
     if num_msgs >= params.min_flush_size
     then
       do
       let (st2, (content2, p)) ←
-        betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
-          content1 st1
+        betree.Internal.flush node params node_id_cnt content1 st1
       let (node1, node_id_cnt1) := p
-      let ⟨ i2, i3, n2, n3 ⟩ := node1
-      let (st3, _) ← betree.store_internal_node i2 content2 st2
-      Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
-        node_id_cnt1))
+      let (st3, _) ← betree.store_internal_node node1.id content2 st2
+      Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_internal_node i content1 st1
-      Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
-        node_id_cnt))
+      let (st2, _) ← betree.store_internal_node node.id content1 st1
+      Result.ok (st2, (betree.Node.Internal node, node_id_cnt))
   | betree.Node.Leaf node =>
     do
     let (st1, content) ← betree.load_leaf_node node.id st
@@ -622,7 +609,7 @@ divergent def betree.Node.apply_messages
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]:
+/- [betree::betree::{betree::betree::Node#5}::apply]:
    Source: 'src/betree.rs', lines 576:4-582:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
@@ -637,7 +624,7 @@ def betree.Node.apply
   let (self1, node_id_cnt1) := p
   Result.ok (st1, (self1, node_id_cnt1))
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
+/- [betree::betree::{betree::betree::BeTree#6}::new]:
    Source: 'src/betree.rs', lines 849:4-849:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
@@ -654,7 +641,7 @@ def betree.BeTree.new
       root := (betree.Node.Leaf { id := id, size := 0#u64 })
     })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
+/- [betree::betree::{betree::betree::BeTree#6}::apply]:
    Source: 'src/betree.rs', lines 868:4-868:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
@@ -666,7 +653,7 @@ def betree.BeTree.apply
   let (n, nic) := p
   Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
+/- [betree::betree::{betree::betree::BeTree#6}::insert]:
    Source: 'src/betree.rs', lines 874:4-874:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
@@ -674,7 +661,7 @@ def betree.BeTree.insert
   :=
   betree.BeTree.apply self key (betree.Message.Insert value) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
+/- [betree::betree::{betree::betree::BeTree#6}::delete]:
    Source: 'src/betree.rs', lines 880:4-880:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) :
@@ -682,7 +669,7 @@ def betree.BeTree.delete
   :=
   betree.BeTree.apply self key betree.Message.Delete st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
+/- [betree::betree::{betree::betree::BeTree#6}::upsert]:
    Source: 'src/betree.rs', lines 886:4-886:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
@@ -691,7 +678,7 @@ def betree.BeTree.upsert
   :=
   betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
+/- [betree::betree::{betree::betree::BeTree#6}::lookup]:
    Source: 'src/betree.rs', lines 895:4-895:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
@@ -701,12 +688,12 @@ def betree.BeTree.lookup
   let (st1, (o, n)) ← betree.Node.lookup self.root key st
   Result.ok (st1, (o, { self with root := n }))
 
-/- [betree_main::main]:
+/- [betree::main]:
    Source: 'src/main.rs', lines 4:0-4:9 -/
 def main : Result Unit :=
   Result.ok ()
 
-/- Unit test for [betree_main::main] -/
+/- Unit test for [betree::main] -/
 #assert (main == Result.ok ())
 
-end betree_main
+end betree
diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/Betree/FunsExternal.lean
index d26177fb..859cbd68 100644
--- a/tests/lean/BetreeMain/FunsExternal.lean
+++ b/tests/lean/Betree/FunsExternal.lean
@@ -1,30 +1,30 @@
--- [betree_main]: external functions.
+-- [betree]: external functions.
 import Base
-import BetreeMain.Types
+import Betree.Types
 open Primitives
-open betree_main
+open betree
 
 -- TODO: fill those bodies
 
-/- [betree_main::betree_utils::load_internal_node] -/
+/- [betree::betree_utils::load_internal_node] -/
 def betree_utils.load_internal_node
   :
   U64 → State → Result (State × (betree.List (U64 × betree.Message))) :=
   fun _ _ => .fail .panic
 
-/- [betree_main::betree_utils::store_internal_node] -/
+/- [betree::betree_utils::store_internal_node] -/
 def betree_utils.store_internal_node
   :
   U64 → betree.List (U64 × betree.Message) → State → Result (State
     × Unit) :=
   fun _ _ _ => .fail .panic
 
-/- [betree_main::betree_utils::load_leaf_node] -/
+/- [betree::betree_utils::load_leaf_node] -/
 def betree_utils.load_leaf_node
   : U64 → State → Result (State × (betree.List (U64 × U64))) :=
   fun _ _ => .fail .panic
 
-/- [betree_main::betree_utils::store_leaf_node] -/
+/- [betree::betree_utils::store_leaf_node] -/
 def betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit) :=
   fun _ _ _ => .fail .panic
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean
index 0dcce5ca..014f0d83 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/Betree/FunsExternal_Template.lean
@@ -1,29 +1,29 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: external functions.
+-- [betree]: external functions.
 -- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
 import Base
-import BetreeMain.Types
+import Betree.Types
 open Primitives
-open betree_main
+open betree
 
-/- [betree_main::betree_utils::load_internal_node]:
+/- [betree::betree_utils::load_internal_node]:
    Source: 'src/betree_utils.rs', lines 98:0-98:63 -/
 axiom betree_utils.load_internal_node
   : U64 → State → Result (State × (betree.List (U64 × betree.Message)))
 
-/- [betree_main::betree_utils::store_internal_node]:
+/- [betree::betree_utils::store_internal_node]:
    Source: 'src/betree_utils.rs', lines 115:0-115:71 -/
 axiom betree_utils.store_internal_node
   :
   U64 → betree.List (U64 × betree.Message) → State → Result (State ×
     Unit)
 
-/- [betree_main::betree_utils::load_leaf_node]:
+/- [betree::betree_utils::load_leaf_node]:
    Source: 'src/betree_utils.rs', lines 132:0-132:55 -/
 axiom betree_utils.load_leaf_node
   : U64 → State → Result (State × (betree.List (U64 × U64)))
 
-/- [betree_main::betree_utils::store_leaf_node]:
+/- [betree::betree_utils::store_leaf_node]:
    Source: 'src/betree_utils.rs', lines 145:0-145:63 -/
 axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/Betree/Types.lean
index 877508f6..3b46c00c 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/Betree/Types.lean
@@ -1,31 +1,31 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: type definitions
+-- [betree]: type definitions
 import Base
-import BetreeMain.TypesExternal
+import Betree.TypesExternal
 open Primitives
 
-namespace betree_main
+namespace betree
 
-/- [betree_main::betree::List]
+/- [betree::betree::List]
    Source: 'src/betree.rs', lines 17:0-17:23 -/
 inductive betree.List (T : Type) :=
 | Cons : T → betree.List T → betree.List T
 | Nil : betree.List T
 
-/- [betree_main::betree::UpsertFunState]
+/- [betree::betree::UpsertFunState]
    Source: 'src/betree.rs', lines 63:0-63:23 -/
 inductive betree.UpsertFunState :=
 | Add : U64 → betree.UpsertFunState
 | Sub : U64 → betree.UpsertFunState
 
-/- [betree_main::betree::Message]
+/- [betree::betree::Message]
    Source: 'src/betree.rs', lines 69:0-69:23 -/
 inductive betree.Message :=
 | Insert : U64 → betree.Message
 | Delete : betree.Message
 | Upsert : betree.UpsertFunState → betree.Message
 
-/- [betree_main::betree::Leaf]
+/- [betree::betree::Leaf]
    Source: 'src/betree.rs', lines 167:0-167:11 -/
 structure betree.Leaf where
   id : U64
@@ -33,12 +33,12 @@ structure betree.Leaf where
 
 mutual
 
-/- [betree_main::betree::Internal]
+/- [betree::betree::Internal]
    Source: 'src/betree.rs', lines 156:0-156:15 -/
 inductive betree.Internal :=
 | mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
 
-/- [betree_main::betree::Node]
+/- [betree::betree::Node]
    Source: 'src/betree.rs', lines 179:0-179:9 -/
 inductive betree.Node :=
 | Internal : betree.Internal → betree.Node
@@ -46,22 +46,38 @@ inductive betree.Node :=
 
 end
 
-/- [betree_main::betree::Params]
+@[simp, reducible]
+def betree.Internal.id (x : betree.Internal) :=
+  match x with | betree.Internal.mk x1 _ _ _ => x1
+
+@[simp, reducible]
+def betree.Internal.pivot (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ x1 _ _ => x1
+
+@[simp, reducible]
+def betree.Internal.left (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ x1 _ => x1
+
+@[simp, reducible]
+def betree.Internal.right (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ _ x1 => x1
+
+/- [betree::betree::Params]
    Source: 'src/betree.rs', lines 187:0-187:13 -/
 structure betree.Params where
   min_flush_size : U64
   split_size : U64
 
-/- [betree_main::betree::NodeIdCounter]
+/- [betree::betree::NodeIdCounter]
    Source: 'src/betree.rs', lines 201:0-201:20 -/
 structure betree.NodeIdCounter where
   next_node_id : U64
 
-/- [betree_main::betree::BeTree]
+/- [betree::betree::BeTree]
    Source: 'src/betree.rs', lines 218:0-218:17 -/
 structure betree.BeTree where
   params : betree.Params
   node_id_cnt : betree.NodeIdCounter
   root : betree.Node
 
-end betree_main
+end betree
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/Betree/TypesExternal.lean
index 1701eaaf..34170271 100644
--- a/tests/lean/BetreeMain/TypesExternal.lean
+++ b/tests/lean/Betree/TypesExternal.lean
@@ -1,4 +1,4 @@
--- [betree_main]: external types.
+-- [betree]: external types.
 import Base
 open Primitives
 
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean
index bbac7e99..12fce657 100644
--- a/tests/lean/BetreeMain/TypesExternal_Template.lean
+++ b/tests/lean/Betree/TypesExternal_Template.lean
@@ -1,5 +1,5 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: external types.
+-- [betree]: external types.
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
diff --git a/tests/lean/BetreeMain.lean b/tests/lean/BetreeMain.lean
deleted file mode 100644
index 5f307877..00000000
--- a/tests/lean/BetreeMain.lean
+++ /dev/null
@@ -1 +0,0 @@
-import BetreeMain.Funs