Regenerate the Coq and Lean betrees

1 files changed, 202 insertions, 89 deletions

diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 8612ccbc..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -79,42 +79,74 @@ def betree.upsert_update
       then prev1 - v
       else Result.ok 0#u64
 
+/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
+   Source: 'src/betree.rs', lines 276:4-284:5 -/
+divergent def betree.List.len_loop
+  (T : Type) (self : betree.List T) (len : U64) : Result U64 :=
+  match self with
+  | betree.List.Cons _ tl =>
+    do
+    let len1 ← len + 1#u64
+    betree.List.len_loop T tl len1
+  | betree.List.Nil => Result.ok 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 :=
+def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
+  betree.List.len_loop T self 0#u64
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
+   Source: 'src/betree.rs', lines 304:4-312:5 -/
+divergent def betree.List.reverse_loop
+  (T : Type) (self : betree.List T) (out : betree.List T) :
+  Result (betree.List T)
+  :=
   match self with
-  | betree.List.Cons _ tl => do
-                             let i ← betree.List.len T tl
-                             1#u64 + i
-  | betree.List.Nil => Result.ok 0#u64
-
-/- [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) :
+  | betree.List.Cons hd tl =>
+    betree.List.reverse_loop T tl (betree.List.Cons hd out)
+  | betree.List.Nil => Result.ok out
+
+/- [betree::betree::{betree::betree::List<T>#1}::reverse]:
+   Source: 'src/betree.rs', lines 304:4-304:32 -/
+def betree.List.reverse
+  (T : Type) (self : betree.List T) : Result (betree.List T) :=
+  betree.List.reverse_loop T self betree.List.Nil
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]: loop 0:
+   Source: 'src/betree.rs', lines 287:4-302:5 -/
+divergent def betree.List.split_at_loop
+  (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n = 0#u64
-  then Result.ok (betree.List.Nil, self)
-  else
+  if n > 0#u64
+  then
     match self with
     | betree.List.Cons hd tl =>
       do
-      let i ← n - 1#u64
-      let p ← betree.List.split_at T tl i
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons hd ls0, ls1)
+      let n1 ← n - 1#u64
+      betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
     | betree.List.Nil => Result.fail .panic
+  else do
+       let l ← betree.List.reverse T beg
+       Result.ok (l, self)
+
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
+   Source: 'src/betree.rs', lines 287:4-287:55 -/
+def betree.List.split_at
+  (T : Type) (self : betree.List T) (n : U64) :
+  Result ((betree.List T) × (betree.List T))
+  :=
+  betree.List.split_at_loop T n betree.List.Nil self
 
 /- [betree::betree::{betree::betree::List<T>#1}::push_front]:
-   Source: 'src/betree.rs', lines 299:4-299:34 -/
+   Source: 'src/betree.rs', lines 315:4-315: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::betree::{betree::betree::List<T>#1}::pop_front]:
-   Source: 'src/betree.rs', lines 306:4-306:32 -/
+   Source: 'src/betree.rs', lines 322:4-322:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
   let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
@@ -123,14 +155,14 @@ def betree.List.pop_front
   | betree.List.Nil => Result.fail .panic
 
 /- [betree::betree::{betree::betree::List<T>#1}::hd]:
-   Source: 'src/betree.rs', lines 318:4-318:22 -/
+   Source: 'src/betree.rs', lines 334:4-334: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::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
-   Source: 'src/betree.rs', lines 327:4-327:44 -/
+   Source: 'src/betree.rs', lines 343:4-343:44 -/
 def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
@@ -138,26 +170,40 @@ def betree.ListPairU64T.head_has_key
                              Result.ok (i = key)
   | betree.List.Nil => Result.ok false
 
-/- [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) :
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: loop 0:
+   Source: 'src/betree.rs', lines 355:4-370:5 -/
+divergent def betree.ListPairU64T.partition_at_pivot_loop
+  (T : Type) (pivot : U64) (beg : betree.List (U64 × T))
+  (end1 : betree.List (U64 × T)) (self : betree.List (U64 × T)) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
   match self with
   | betree.List.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
-    then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
+    then
+      betree.ListPairU64T.partition_at_pivot_loop T pivot beg (betree.List.Cons
+        (i, t) end1) tl
     else
-      do
-      let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
-      let (ls0, ls1) := p
-      Result.ok (betree.List.Cons (i, t) ls0, ls1)
-  | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
+      betree.ListPairU64T.partition_at_pivot_loop T pivot (betree.List.Cons (i,
+        t) beg) end1 tl
+  | betree.List.Nil =>
+    do
+    let l ← betree.List.reverse (U64 × T) beg
+    let l1 ← betree.List.reverse (U64 × T) end1
+    Result.ok (l, l1)
+
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
+   Source: 'src/betree.rs', lines 355:4-355:73 -/
+def betree.ListPairU64T.partition_at_pivot
+  (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
+  Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
+  :=
+  betree.ListPairU64T.partition_at_pivot_loop T pivot betree.List.Nil
+    betree.List.Nil self
 
 /- [betree::betree::{betree::betree::Leaf#3}::split]:
-   Source: 'src/betree.rs', lines 359:4-364:17 -/
+   Source: 'src/betree.rs', lines 378:4-383:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -176,9 +222,9 @@ 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::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
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 792:4-810:5 -/
+divergent def betree.Node.lookup_first_message_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -190,19 +236,28 @@ divergent def betree.Node.lookup_first_message_for_key
     then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
     else
       do
-      let (l, lookup_first_message_for_key_back) ←
-        betree.Node.lookup_first_message_for_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_for_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_for_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (i, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [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
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
+   Source: 'src/betree.rs', lines 792:4-795:34 -/
+def betree.Node.lookup_first_message_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 649:4-660:5 -/
+divergent def betree.Node.lookup_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   match bindings with
   | betree.List.Cons hd tl =>
@@ -212,12 +267,18 @@ divergent def betree.Node.lookup_in_bindings
     else
       if i > key
       then Result.ok none
-      else betree.Node.lookup_in_bindings key tl
+      else betree.Node.lookup_in_bindings_loop key tl
   | betree.List.Nil => Result.ok none
 
-/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
-   Source: 'src/betree.rs', lines 819:4-819:90 -/
-divergent def betree.Node.apply_upserts
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
+   Source: 'src/betree.rs', lines 649:4-649:84 -/
+def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  betree.Node.lookup_in_bindings_loop key bindings
+
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]: loop 0:
+   Source: 'src/betree.rs', lines 820:4-844:5 -/
+divergent def betree.Node.apply_upserts_loop
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   :
   Result (U64 × (betree.List (U64 × betree.Message)))
@@ -235,7 +296,7 @@ divergent def betree.Node.apply_upserts
     | betree.Message.Upsert s =>
       do
       let v ← betree.upsert_update prev s
-      betree.Node.apply_upserts msgs1 (some v) key
+      betree.Node.apply_upserts_loop msgs1 (some v) key
   else
     do
     let v ← core.option.Option.unwrap U64 prev
@@ -244,8 +305,17 @@ divergent def betree.Node.apply_upserts
         betree.Message.Insert v)
     Result.ok (v, msgs1)
 
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
+   Source: 'src/betree.rs', lines 820:4-820:94 -/
+def betree.Node.apply_upserts
+  (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
+  :
+  Result (U64 × (betree.List (U64 × betree.Message)))
+  :=
+  betree.Node.apply_upserts_loop msgs prev key
+
 /- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
-   Source: 'src/betree.rs', lines 395:4-395:63 -/
+   Source: 'src/betree.rs', lines 414:4-414:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
@@ -261,7 +331,7 @@ mutual divergent def betree.Internal.lookup_in_children
     Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
 /- [betree::betree::{betree::betree::Node#5}::lookup]:
-   Source: 'src/betree.rs', lines 709:4-709:58 -/
+   Source: 'src/betree.rs', lines 712:4-712:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Node))
@@ -320,9 +390,9 @@ divergent def betree.Node.lookup
 
 end
 
-/- [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
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: loop 0:
+   Source: 'src/betree.rs', lines 683:4-692:5 -/
+divergent def betree.Node.filter_messages_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
@@ -335,13 +405,21 @@ divergent def betree.Node.filter_messages_for_key
       let (_, msgs1) ←
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
-      betree.Node.filter_messages_for_key key msgs1
+      betree.Node.filter_messages_for_key_loop key msgs1
     else Result.ok (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ok betree.List.Nil
 
-/- [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
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
+   Source: 'src/betree.rs', lines 683:4-683:77 -/
+def betree.Node.filter_messages_for_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.filter_messages_for_key_loop key msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: loop 0:
+   Source: 'src/betree.rs', lines 694:4-706:5 -/
+divergent def betree.Node.lookup_first_message_after_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
     betree.Message) → Result (betree.List (U64 × betree.Message))))
@@ -352,19 +430,28 @@ divergent def betree.Node.lookup_first_message_after_key
     if k = key
     then
       do
-      let (l, lookup_first_message_after_key_back) ←
-        betree.Node.lookup_first_message_after_key key next_msgs
-      let back :=
+      let (l, back) ←
+        betree.Node.lookup_first_message_after_key_loop key next_msgs
+      let back1 :=
         fun ret =>
           do
-          let next_msgs1 ← lookup_first_message_after_key_back ret
+          let next_msgs1 ← back ret
           Result.ok (betree.List.Cons (k, m) next_msgs1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
     else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
+   Source: 'src/betree.rs', lines 694:4-697:34 -/
+def betree.Node.lookup_first_message_after_key
+  (key : U64) (msgs : betree.List (U64 × betree.Message)) :
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
+  :=
+  betree.Node.lookup_first_message_after_key_loop key msgs
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
-   Source: 'src/betree.rs', lines 521:4-521:89 -/
+   Source: 'src/betree.rs', lines 534:4-534:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
   (new_msg : betree.Message) :
@@ -427,9 +514,9 @@ 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::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
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: loop 0:
+   Source: 'src/betree.rs', lines 518:4-526:5 -/
+divergent def betree.Node.apply_messages_to_internal_loop
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -439,12 +526,21 @@ divergent def betree.Node.apply_messages_to_internal
     do
     let (i, m) := new_msg
     let msgs1 ← betree.Node.apply_to_internal msgs i m
-    betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
+    betree.Node.apply_messages_to_internal_loop msgs1 new_msgs_tl
   | betree.List.Nil => Result.ok msgs
 
-/- [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
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
+   Source: 'src/betree.rs', lines 518:4-521:5 -/
+def betree.Node.apply_messages_to_internal
+  (msgs : betree.List (U64 × betree.Message))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × betree.Message))
+  :=
+  betree.Node.apply_messages_to_internal_loop msgs new_msgs
+
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 664:4-677:5 -/
+divergent def betree.Node.lookup_mut_in_bindings_loop
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
     (betree.List (U64 × U64))))
@@ -456,18 +552,26 @@ divergent def betree.Node.lookup_mut_in_bindings
     then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
     else
       do
-      let (l, lookup_mut_in_bindings_back) ←
-        betree.Node.lookup_mut_in_bindings key tl
-      let back :=
+      let (l, back) ← betree.Node.lookup_mut_in_bindings_loop key tl
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← lookup_mut_in_bindings_back ret
+          let tl1 ← back ret
           Result.ok (betree.List.Cons (i, i1) tl1)
-      Result.ok (l, back)
+      Result.ok (l, back1)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
+   Source: 'src/betree.rs', lines 664:4-667:32 -/
+def betree.Node.lookup_mut_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) :
+  Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
+    (betree.List (U64 × U64))))
+  :=
+  betree.Node.lookup_mut_in_bindings_loop key bindings
+
 /- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
-   Source: 'src/betree.rs', lines 460:4-460:87 -/
+   Source: 'src/betree.rs', lines 476:4-476:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
   :
@@ -506,9 +610,9 @@ def betree.Node.apply_to_leaf
       let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
       lookup_mut_in_bindings_back bindings2
 
-/- [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
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: loop 0:
+   Source: 'src/betree.rs', lines 463:4-471:5 -/
+divergent def betree.Node.apply_messages_to_leaf_loop
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × U64))
@@ -518,11 +622,20 @@ divergent def betree.Node.apply_messages_to_leaf
     do
     let (i, m) := new_msg
     let bindings1 ← betree.Node.apply_to_leaf bindings i m
-    betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
+    betree.Node.apply_messages_to_leaf_loop bindings1 new_msgs_tl
   | betree.List.Nil => Result.ok bindings
 
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
+   Source: 'src/betree.rs', lines 463:4-466:5 -/
+def betree.Node.apply_messages_to_leaf
+  (bindings : betree.List (U64 × U64))
+  (new_msgs : betree.List (U64 × betree.Message)) :
+  Result (betree.List (U64 × U64))
+  :=
+  betree.Node.apply_messages_to_leaf_loop bindings new_msgs
+
 /- [betree::betree::{betree::betree::Internal#4}::flush]:
-   Source: 'src/betree.rs', lines 410:4-415:26 -/
+   Source: 'src/betree.rs', lines 429:4-434:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -563,7 +676,7 @@ mutual divergent def betree.Internal.flush
       self.left n, node_id_cnt1)))
 
 /- [betree::betree::{betree::betree::Node#5}::apply_messages]:
-   Source: 'src/betree.rs', lines 588:4-593:5 -/
+   Source: 'src/betree.rs', lines 601:4-606:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -610,7 +723,7 @@ divergent def betree.Node.apply_messages
 end
 
 /- [betree::betree::{betree::betree::Node#5}::apply]:
-   Source: 'src/betree.rs', lines 576:4-582:5 -/
+   Source: 'src/betree.rs', lines 589:4-595:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -625,7 +738,7 @@ def betree.Node.apply
   Result.ok (st1, (self1, node_id_cnt1))
 
 /- [betree::betree::{betree::betree::BeTree#6}::new]:
-   Source: 'src/betree.rs', lines 849:4-849:60 -/
+   Source: 'src/betree.rs', lines 848:4-848:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -642,7 +755,7 @@ def betree.BeTree.new
     })
 
 /- [betree::betree::{betree::betree::BeTree#6}::apply]:
-   Source: 'src/betree.rs', lines 868:4-868:47 -/
+   Source: 'src/betree.rs', lines 867:4-867:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × betree.BeTree)
@@ -654,7 +767,7 @@ def betree.BeTree.apply
   Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
 /- [betree::betree::{betree::betree::BeTree#6}::insert]:
-   Source: 'src/betree.rs', lines 874:4-874:52 -/
+   Source: 'src/betree.rs', lines 873:4-873:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -662,7 +775,7 @@ def betree.BeTree.insert
   betree.BeTree.apply self key (betree.Message.Insert value) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::delete]:
-   Source: 'src/betree.rs', lines 880:4-880:38 -/
+   Source: 'src/betree.rs', lines 879:4-879:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -670,7 +783,7 @@ def betree.BeTree.delete
   betree.BeTree.apply self key betree.Message.Delete st
 
 /- [betree::betree::{betree::betree::BeTree#6}::upsert]:
-   Source: 'src/betree.rs', lines 886:4-886:59 -/
+   Source: 'src/betree.rs', lines 885:4-885:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -679,7 +792,7 @@ def betree.BeTree.upsert
   betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
 /- [betree::betree::{betree::betree::BeTree#6}::lookup]:
-   Source: 'src/betree.rs', lines 895:4-895:62 -/
+   Source: 'src/betree.rs', lines 894:4-894:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.BeTree))