From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/lean/BetreeMain/Funs.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 07ef08dc..6681731f 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -64,11 +64,6 @@ def betree.NodeIdCounter.fresh_id_back
     let i ← self.next_node_id + (U64.ofInt 1)
     Result.ret { next_node_id := i }
 
-/- [core::num::u64::{9}::MAX] -/
-def core_num_u64_max_body : Result U64 :=
-  Result.ret (U64.ofInt 18446744073709551615)
-def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
-
 /- [betree_main::betree::upsert_update]: forward function -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -81,10 +76,10 @@ def betree.upsert_update
     match st with
     | betree.UpsertFunState.Add v =>
       do
-        let margin ← core_num_u64_max_c - prev0
+        let margin ← core_u64_max - prev0
         if margin >= v
         then prev0 + v
-        else Result.ret core_num_u64_max_c
+        else Result.ret core_u64_max
     | betree.UpsertFunState.Sub v =>
       if prev0 >= v
       then prev0 - v
-- 
cgit v1.2.3


From 76e7a6e4c4ead2e48bc56118b38347b59f4f30db Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 14:50:57 +0200
Subject: Regenerate the betree example for Lean

---
 tests/lean/BetreeMain/Funs.lean | 79 ++++++++++++++++++++---------------------
 1 file changed, 39 insertions(+), 40 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 6681731f..0901d449 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -40,39 +40,39 @@ def betree.store_leaf_node
 /- [betree_main::betree::fresh_node_id]: forward function -/
 def betree.fresh_node_id (counter : U64) : Result U64 :=
   do
-    let _ ← counter + (U64.ofInt 1)
+    let _ ← counter + 1#u64
     Result.ret counter
 
 /- [betree_main::betree::fresh_node_id]: backward function 0 -/
 def betree.fresh_node_id_back (counter : U64) : Result U64 :=
-  counter + (U64.ofInt 1)
+  counter + 1#u64
 
 /- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
-  Result.ret { next_node_id := (U64.ofInt 0) }
+  Result.ret { next_node_id := 0#u64 }
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
-    let _ ← self.next_node_id + (U64.ofInt 1)
+    let _ ← self.next_node_id + 1#u64
     Result.ret self.next_node_id
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
-    let i ← self.next_node_id + (U64.ofInt 1)
+    let i ← self.next_node_id + 1#u64
     Result.ret { next_node_id := i }
 
 /- [betree_main::betree::upsert_update]: forward function -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
   match prev with
-  | Option.none =>
+  | none =>
     match st with
     | betree.UpsertFunState.Add v => Result.ret v
-    | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0)
-  | Option.some prev0 =>
+    | betree.UpsertFunState.Sub i => Result.ret 0#u64
+  | some prev0 =>
     match st with
     | betree.UpsertFunState.Add v =>
       do
@@ -83,29 +83,28 @@ def betree.upsert_update
     | betree.UpsertFunState.Sub v =>
       if prev0 >= v
       then prev0 - v
-      else Result.ret (U64.ofInt 0)
+      else Result.ret 0#u64
 
 /- [betree_main::betree::List::{1}::len]: forward function -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
-  | betree.List.Cons t tl =>
-    do
-      let i ← betree.List.len T tl
-      (U64.ofInt 1) + i
-  | betree.List.Nil => Result.ret (U64.ofInt 0)
+  | betree.List.Cons t tl => do
+                               let i ← betree.List.len T tl
+                               1#u64 + i
+  | betree.List.Nil => Result.ret 0#u64
 
 /- [betree_main::betree::List::{1}::split_at]: forward function -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n = (U64.ofInt 0)
+  if n = 0#u64
   then Result.ret (betree.List.Nil, self)
   else
     match self with
     | betree.List.Cons hd tl =>
       do
-        let i ← n - (U64.ofInt 1)
+        let i ← n - 1#u64
         let p ← betree.List.split_at T tl i
         let (ls0, ls1) := p
         let l := ls0
@@ -116,13 +115,13 @@ divergent def betree.List.split_at
    (there is a single backward function, and the forward function returns ()) -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
-  let tl := mem.replace (betree.List T) self betree.List.Nil
+  let tl := core.mem.replace (betree.List T) self betree.List.Nil
   let l := tl
   Result.ret (betree.List.Cons x l)
 
 /- [betree_main::betree::List::{1}::pop_front]: forward function -/
 def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
-  let ls := mem.replace (betree.List T) self betree.List.Nil
+  let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
   | betree.List.Nil => Result.fail Error.panic
@@ -130,7 +129,7 @@ def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
 /- [betree_main::betree::List::{1}::pop_front]: backward function 0 -/
 def betree.List.pop_front_back
   (T : Type) (self : betree.List T) : Result (betree.List T) :=
-  let ls := mem.replace (betree.List T) self betree.List.Nil
+  let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret tl
   | betree.List.Nil => Result.fail Error.panic
@@ -256,7 +255,7 @@ divergent def betree.Node.apply_upserts
             let v ← betree.upsert_update prev s
             let msgs0 ←
               betree.List.pop_front_back (U64 × betree.Message) msgs
-            betree.Node.apply_upserts msgs0 (Option.some v) key st
+            betree.Node.apply_upserts msgs0 (some v) key st
     else
       do
         let (st0, v) ← core.option.Option.unwrap U64 prev st
@@ -286,7 +285,7 @@ divergent def betree.Node.apply_upserts_back
             let v ← betree.upsert_update prev s
             let msgs0 ←
               betree.List.pop_front_back (U64 × betree.Message) msgs
-            betree.Node.apply_upserts_back msgs0 (Option.some v) key st
+            betree.Node.apply_upserts_back msgs0 (some v) key st
     else
       do
         let (_, v) ← core.option.Option.unwrap U64 prev st
@@ -300,12 +299,12 @@ divergent def betree.Node.lookup_in_bindings
   | betree.List.Cons hd tl =>
     let (i, i0) := hd
     if i = key
-    then Result.ret (Option.some i0)
+    then Result.ret (some i0)
     else
       if i > key
-      then Result.ret Option.none
+      then Result.ret none
       else betree.Node.lookup_in_bindings key tl
-  | betree.List.Nil => Result.ret Option.none
+  | betree.List.Nil => Result.ret none
 
 /- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
 mutual divergent def betree.Internal.lookup_in_children
@@ -348,13 +347,13 @@ divergent def betree.Node.lookup
         if k != key
         then
           do
-            let (st1, opt) ←
+            let (st1, o) ←
               betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
                 key st0
             let _ ←
               betree.Node.lookup_first_message_for_key_back key msgs
                 (betree.List.Cons (k, msg) l)
-            Result.ret (st1, opt)
+            Result.ret (st1, o)
         else
           match msg with
           | betree.Message.Insert v =>
@@ -362,13 +361,13 @@ divergent def betree.Node.lookup
               let _ ←
                 betree.Node.lookup_first_message_for_key_back key msgs
                   (betree.List.Cons (k, betree.Message.Insert v) l)
-              Result.ret (st0, Option.some v)
+              Result.ret (st0, some v)
           | betree.Message.Delete =>
             do
               let _ ←
                 betree.Node.lookup_first_message_for_key_back key msgs
                   (betree.List.Cons (k, betree.Message.Delete) l)
-              Result.ret (st0, Option.none)
+              Result.ret (st0, none)
           | betree.Message.Upsert ufs =>
             do
               let (st1, v) ←
@@ -387,21 +386,21 @@ divergent def betree.Node.lookup
               let msgs0 ←
                 betree.Node.lookup_first_message_for_key_back key msgs pending0
               let (st3, _) ← betree.store_internal_node i1 msgs0 st2
-              Result.ret (st3, Option.some v0)
+              Result.ret (st3, some v0)
       | betree.List.Nil =>
         do
-          let (st1, opt) ←
+          let (st1, o) ←
             betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
               key st0
           let _ ←
             betree.Node.lookup_first_message_for_key_back key msgs
               betree.List.Nil
-          Result.ret (st1, opt)
+          Result.ret (st1, o)
   | betree.Node.Leaf node =>
     do
       let (st0, bindings) ← betree.load_leaf_node node.id st
-      let opt ← betree.Node.lookup_in_bindings key bindings
-      Result.ret (st0, opt)
+      let o ← betree.Node.lookup_in_bindings key bindings
+      Result.ret (st0, o)
 
 /- [betree_main::betree::Node::{5}::lookup]: backward function 0 -/
 divergent def betree.Node.lookup_back
@@ -560,7 +559,7 @@ def betree.Node.apply_to_internal
           match m with
           | betree.Message.Insert prev =>
             do
-              let v ← betree.upsert_update (Option.some prev) s
+              let v ← betree.upsert_update (some prev) s
               let msgs1 ←
                 betree.List.pop_front_back (U64 × betree.Message) msgs0
               let msgs2 ←
@@ -569,7 +568,7 @@ def betree.Node.apply_to_internal
               betree.Node.lookup_first_message_for_key_back key msgs msgs2
           | betree.Message.Delete =>
             do
-              let v ← betree.upsert_update Option.none s
+              let v ← betree.upsert_update none s
               let msgs1 ←
                 betree.List.pop_front_back (U64 × betree.Message) msgs0
               let msgs2 ←
@@ -665,7 +664,7 @@ def betree.Node.apply_to_leaf
         | betree.Message.Upsert s =>
           do
             let (_, i) := hd
-            let v ← betree.upsert_update (Option.some i) s
+            let v ← betree.upsert_update (some i) s
             let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
             let bindings2 ←
               betree.List.push_front (U64 × U64) bindings1 (key, v)
@@ -681,7 +680,7 @@ def betree.Node.apply_to_leaf
         betree.Node.lookup_mut_in_bindings_back key bindings bindings0
       | betree.Message.Upsert s =>
         do
-          let v ← betree.upsert_update Option.none s
+          let v ← betree.upsert_update none s
           let bindings1 ←
             betree.List.push_front (U64 × U64) bindings0 (key, v)
           betree.Node.lookup_mut_in_bindings_back key bindings bindings1
@@ -808,7 +807,7 @@ divergent def betree.Node.apply_messages
       let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2) * params.split_size
+      let i ← 2#u64 * params.split_size
       if len >= i
       then
         do
@@ -858,7 +857,7 @@ divergent def betree.Node.apply_messages_back
       let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2) * params.split_size
+      let i ← 2#u64 * params.split_size
       if len >= i
       then
         do
@@ -918,7 +917,7 @@ def betree.BeTree.new
         params :=
           { min_flush_size := min_flush_size, split_size := split_size },
         node_id_cnt := node_id_cnt0,
-        root := (betree.Node.Leaf { id := id, size := (U64.ofInt 0) })
+        root := (betree.Node.Leaf { id := id, size := 0#u64 })
       })
 
 /- [betree_main::betree::BeTree::{6}::apply]: forward function -/
-- 
cgit v1.2.3


From 753f7e72f87f5282aee60ad5ada47efeb42625e9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 11:50:44 +0100
Subject: Regenerate the betree files

---
 tests/lean/BetreeMain/Funs.lean                  | 114 +++++++++++------------
 tests/lean/BetreeMain/FunsExternal_Template.lean |   2 +-
 2 files changed, 58 insertions(+), 58 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0901d449..441a3721 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -47,17 +47,17 @@ def betree.fresh_node_id (counter : U64) : Result U64 :=
 def betree.fresh_node_id_back (counter : U64) : Result U64 :=
   counter + 1#u64
 
-/- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ret { next_node_id := 0#u64 }
 
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
     let _ ← self.next_node_id + 1#u64
     Result.ret self.next_node_id
 
-/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
@@ -85,7 +85,7 @@ def betree.upsert_update
       then prev0 - v
       else Result.ret 0#u64
 
-/- [betree_main::betree::List::{1}::len]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
   | betree.List.Cons t tl => do
@@ -93,7 +93,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
                                1#u64 + i
   | betree.List.Nil => Result.ret 0#u64
 
-/- [betree_main::betree::List::{1}::split_at]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
   Result ((betree.List T) × (betree.List T))
@@ -111,7 +111,7 @@ divergent def betree.List.split_at
         Result.ret (betree.List.Cons hd l, ls1)
     | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{1}::push_front]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
@@ -119,14 +119,14 @@ def betree.List.push_front
   let l := tl
   Result.ret (betree.List.Cons x l)
 
-/- [betree_main::betree::List::{1}::pop_front]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function -/
 def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{1}::pop_front]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 -/
 def betree.List.pop_front_back
   (T : Type) (self : betree.List T) : Result (betree.List T) :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
@@ -134,22 +134,22 @@ def betree.List.pop_front_back
   | betree.List.Cons x tl => Result.ret tl
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{1}::hd]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd l => Result.ret hd
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::List::{2}::head_has_key]: forward function -/
-def betree.List.head_has_key
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function -/
+def betree.ListTupleU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
   | betree.List.Cons hd l => let (i, _) := hd
                              Result.ret (i = key)
   | betree.List.Nil => Result.ret false
 
-/- [betree_main::betree::List::{2}::partition_at_pivot]: forward function -/
-divergent def betree.List.partition_at_pivot
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function -/
+divergent def betree.ListTupleU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
   :=
@@ -160,13 +160,13 @@ divergent def betree.List.partition_at_pivot
     then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
-        let p ← betree.List.partition_at_pivot T tl pivot
+        let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
         let (ls0, ls1) := p
         let l := ls0
         Result.ret (betree.List.Cons (i, t) l, ls1)
   | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::Leaf::{3}::split]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -186,7 +186,7 @@ def betree.Leaf.split
     let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
     Result.ret (st1, betree.Internal.mk self.id pivot n n0)
 
-/- [betree_main::betree::Leaf::{3}::split]: backward function 2 -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 -/
 def betree.Leaf.split_back
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -203,7 +203,7 @@ def betree.Leaf.split_back
     let _ ← betree.store_leaf_node id1 content1 st0
     betree.NodeIdCounter.fresh_id_back node_id_cnt0
 
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function -/
 divergent def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -216,7 +216,7 @@ divergent def betree.Node.lookup_first_message_for_key
     else betree.Node.lookup_first_message_for_key key next_msgs
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 -/
 divergent def betree.Node.lookup_first_message_for_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -234,14 +234,14 @@ divergent def betree.Node.lookup_first_message_for_key_back
         Result.ret (betree.List.Cons (i, m) next_msgs0)
   | betree.List.Nil => Result.ret ret0
 
-/- [betree_main::betree::Node::{5}::apply_upserts]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
   Result (State × U64)
   :=
   do
-    let b ← betree.List.head_has_key betree.Message msgs key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
     if b
     then
       do
@@ -264,14 +264,14 @@ divergent def betree.Node.apply_upserts
             betree.Message.Insert v)
         Result.ret (st0, v)
 
-/- [betree_main::betree::Node::{5}::apply_upserts]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 -/
 divergent def betree.Node.apply_upserts_back
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
   Result (betree.List (U64 × betree.Message))
   :=
   do
-    let b ← betree.List.head_has_key betree.Message msgs key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
     if b
     then
       do
@@ -292,7 +292,7 @@ divergent def betree.Node.apply_upserts_back
         betree.List.push_front (U64 × betree.Message) msgs (key,
           betree.Message.Insert v)
 
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function -/
 divergent def betree.Node.lookup_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
   match bindings with
@@ -306,7 +306,7 @@ divergent def betree.Node.lookup_in_bindings
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ret none
 
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × (Option U64))
@@ -316,7 +316,7 @@ mutual divergent def betree.Internal.lookup_in_children
   then betree.Node.lookup n key st
   else betree.Node.lookup n0 key st
 
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 -/
 divergent def betree.Internal.lookup_in_children_back
   (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
   let ⟨ i, i0, n, n0 ⟩ := self
@@ -330,7 +330,7 @@ divergent def betree.Internal.lookup_in_children_back
       let n1 ← betree.Node.lookup_back n0 key st
       Result.ret (betree.Internal.mk i i0 n n1)
 
-/- [betree_main::betree::Node::{5}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × (Option U64))
@@ -402,7 +402,7 @@ divergent def betree.Node.lookup
       let o ← betree.Node.lookup_in_bindings key bindings
       Result.ret (st0, o)
 
-/- [betree_main::betree::Node::{5}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 -/
 divergent def betree.Node.lookup_back
   (self : betree.Node) (key : U64) (st : State) : Result betree.Node :=
   match self with
@@ -475,7 +475,7 @@ divergent def betree.Node.lookup_back
 
 end
 
-/- [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -494,7 +494,7 @@ divergent def betree.Node.filter_messages_for_key
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function -/
 divergent def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
@@ -507,7 +507,7 @@ divergent def betree.Node.lookup_first_message_after_key
     else Result.ret (betree.List.Cons (k, m) next_msgs)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 -/
 divergent def betree.Node.lookup_first_message_after_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -525,7 +525,7 @@ divergent def betree.Node.lookup_first_message_after_key_back
     else Result.ret ret0
   | betree.List.Nil => Result.ret ret0
 
-/- [betree_main::betree::Node::{5}::apply_to_internal]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
@@ -534,7 +534,7 @@ def betree.Node.apply_to_internal
   :=
   do
     let msgs0 ← betree.Node.lookup_first_message_for_key key msgs
-    let b ← betree.List.head_has_key betree.Message msgs0 key
+    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key
     if b
     then
       match new_msg with
@@ -591,7 +591,7 @@ def betree.Node.apply_to_internal
           betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg)
         betree.Node.lookup_first_message_for_key_back key msgs msgs1
 
-/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
@@ -606,7 +606,7 @@ divergent def betree.Node.apply_messages_to_internal
       betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function -/
 divergent def betree.Node.lookup_mut_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result (betree.List (U64 × U64))
@@ -619,7 +619,7 @@ divergent def betree.Node.lookup_mut_in_bindings
     else betree.Node.lookup_mut_in_bindings key tl
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 -/
 divergent def betree.Node.lookup_mut_in_bindings_back
   (key : U64) (bindings : betree.List (U64 × U64))
   (ret0 : betree.List (U64 × U64)) :
@@ -636,7 +636,7 @@ divergent def betree.Node.lookup_mut_in_bindings_back
         Result.ret (betree.List.Cons (i, i0) tl0)
   | betree.List.Nil => Result.ret ret0
 
-/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
@@ -645,7 +645,7 @@ def betree.Node.apply_to_leaf
   :=
   do
     let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
-    let b ← betree.List.head_has_key U64 bindings0 key
+    let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key
     if b
     then
       do
@@ -685,7 +685,7 @@ def betree.Node.apply_to_leaf
             betree.List.push_front (U64 × U64) bindings0 (key, v)
           betree.Node.lookup_mut_in_bindings_back key bindings bindings1
 
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
@@ -700,7 +700,7 @@ divergent def betree.Node.apply_messages_to_leaf
       betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -709,7 +709,7 @@ mutual divergent def betree.Internal.flush
   :=
   do
     let ⟨ _, i, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i
+    let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i
     let (msgs_left, msgs_right) := p
     let len_left ← betree.List.len (U64 × betree.Message) msgs_left
     if len_left >= params.min_flush_size
@@ -738,7 +738,7 @@ mutual divergent def betree.Internal.flush
           betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
         Result.ret (st0, msgs_left)
 
-/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 -/
 divergent def betree.Internal.flush_back
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -747,7 +747,7 @@ divergent def betree.Internal.flush_back
   :=
   do
     let ⟨ i, i0, n, n0 ⟩ := self
-    let p ← betree.List.partition_at_pivot betree.Message content i0
+    let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i0
     let (msgs_left, msgs_right) := p
     let len_left ← betree.List.len (U64 × betree.Message) msgs_left
     if len_left >= params.min_flush_size
@@ -772,7 +772,7 @@ divergent def betree.Internal.flush_back
           betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
         Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
 
-/- [betree_main::betree::Node::{5}::apply_messages]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -820,7 +820,7 @@ divergent def betree.Node.apply_messages
           let (st1, _) ← betree.store_leaf_node node.id content0 st0
           Result.ret (st1, ())
 
-/- [betree_main::betree::Node::{5}::apply_messages]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 -/
 divergent def betree.Node.apply_messages_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -874,7 +874,7 @@ divergent def betree.Node.apply_messages_back
 
 end
 
-/- [betree_main::betree::Node::{5}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -891,7 +891,7 @@ def betree.Node.apply
         (key, new_msg) l) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::Node::{5}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 -/
 def betree.Node.apply_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -902,7 +902,7 @@ def betree.Node.apply_back
   betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons
     (key, new_msg) l) st
 
-/- [betree_main::betree::BeTree::{6}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -920,7 +920,7 @@ def betree.BeTree.new
         root := (betree.Node.Leaf { id := id, size := 0#u64 })
       })
 
-/- [betree_main::betree::BeTree::{6}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × Unit)
@@ -932,7 +932,7 @@ def betree.BeTree.apply
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 -/
 def betree.BeTree.apply_back
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result betree.BeTree
@@ -942,7 +942,7 @@ def betree.BeTree.apply_back
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret { self with node_id_cnt := nic, root := n }
 
-/- [betree_main::betree::BeTree::{6}::insert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × Unit)
@@ -954,14 +954,14 @@ def betree.BeTree.insert
       betree.BeTree.apply_back self key (betree.Message.Insert value) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::insert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 -/
 def betree.BeTree.insert_back
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result betree.BeTree
   :=
   betree.BeTree.apply_back self key (betree.Message.Insert value) st
 
-/- [betree_main::betree::BeTree::{6}::delete]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) :=
   do
@@ -969,12 +969,12 @@ def betree.BeTree.delete
     let _ ← betree.BeTree.apply_back self key betree.Message.Delete st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::delete]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 -/
 def betree.BeTree.delete_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   betree.BeTree.apply_back self key betree.Message.Delete st
 
-/- [betree_main::betree::BeTree::{6}::upsert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -986,7 +986,7 @@ def betree.BeTree.upsert
     let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::BeTree::{6}::upsert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 -/
 def betree.BeTree.upsert_back
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -994,14 +994,14 @@ def betree.BeTree.upsert_back
   :=
   betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
 
-/- [betree_main::betree::BeTree::{6}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
   betree.Node.lookup self.root key st
 
-/- [betree_main::betree::BeTree::{6}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 -/
 def betree.BeTree.lookup_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   do
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index 430d2dda..1dc3af0e 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -24,7 +24,7 @@ axiom betree_utils.load_leaf_node
 axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
 
-/- [core::option::Option::{0}::unwrap]: forward function -/
+/- [core::option::{core::option::Option<T>}::unwrap]: forward function -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)
 
-- 
cgit v1.2.3


From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:57:38 +0100
Subject: Regenerate the files

---
 tests/lean/BetreeMain/Funs.lean                  | 168 +++++++++++++++--------
 tests/lean/BetreeMain/FunsExternal_Template.lean |  15 +-
 tests/lean/BetreeMain/Types.lean                 |  27 ++--
 3 files changed, 140 insertions(+), 70 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 441a3721..45548884 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -7,14 +7,16 @@ open Primitives
 
 namespace betree_main
 
-/- [betree_main::betree::load_internal_node]: forward function -/
+/- [betree_main::betree::load_internal_node]: forward function
+   Source: 'src/betree.rs', lines 36:0-36:52 -/
 def betree.load_internal_node
   (id : U64) (st : State) :
   Result (State × (betree.List (U64 × betree.Message)))
   :=
   betree_utils.load_internal_node id st
 
-/- [betree_main::betree::store_internal_node]: forward function -/
+/- [betree_main::betree::store_internal_node]: forward function
+   Source: 'src/betree.rs', lines 41:0-41:60 -/
 def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
   Result (State × Unit)
@@ -23,12 +25,14 @@ def betree.store_internal_node
     let (st0, _) ← betree_utils.store_internal_node id content st
     Result.ret (st0, ())
 
-/- [betree_main::betree::load_leaf_node]: forward function -/
+/- [betree_main::betree::load_leaf_node]: forward function
+   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]: forward function -/
+/- [betree_main::betree::store_leaf_node]: forward function
+   Source: 'src/betree.rs', lines 51:0-51:52 -/
 def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
   Result (State × Unit)
@@ -37,34 +41,40 @@ def betree.store_leaf_node
     let (st0, _) ← betree_utils.store_leaf_node id content st
     Result.ret (st0, ())
 
-/- [betree_main::betree::fresh_node_id]: forward function -/
+/- [betree_main::betree::fresh_node_id]: forward function
+   Source: 'src/betree.rs', lines 55:0-55:48 -/
 def betree.fresh_node_id (counter : U64) : Result U64 :=
   do
     let _ ← counter + 1#u64
     Result.ret counter
 
-/- [betree_main::betree::fresh_node_id]: backward function 0 -/
+/- [betree_main::betree::fresh_node_id]: backward function 0
+   Source: 'src/betree.rs', lines 55:0-55:48 -/
 def betree.fresh_node_id_back (counter : U64) : Result U64 :=
   counter + 1#u64
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+   Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ret { next_node_id := 0#u64 }
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+   Source: 'src/betree.rs', lines 210:4-210:36 -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
     let _ ← self.next_node_id + 1#u64
     Result.ret self.next_node_id
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
+   Source: 'src/betree.rs', lines 210:4-210:36 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
     let i ← self.next_node_id + 1#u64
     Result.ret { next_node_id := i }
 
-/- [betree_main::betree::upsert_update]: forward function -/
+/- [betree_main::betree::upsert_update]: forward function
+   Source: 'src/betree.rs', lines 234:0-234:70 -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
   match prev with
@@ -85,7 +95,8 @@ def betree.upsert_update
       then prev0 - v
       else Result.ret 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+   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
   | betree.List.Cons t tl => do
@@ -93,7 +104,8 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
                                1#u64 + i
   | betree.List.Nil => Result.ret 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+   Source: 'src/betree.rs', lines 284:4-284:51 -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
   Result ((betree.List T) × (betree.List T))
@@ -112,21 +124,24 @@ divergent def betree.List.split_at
     | betree.List.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   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
   let l := tl
   Result.ret (betree.List.Cons x l)
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
+   Source: 'src/betree.rs', lines 306:4-306:32 -/
 def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+   Source: 'src/betree.rs', lines 306:4-306:32 -/
 def betree.List.pop_front_back
   (T : Type) (self : betree.List T) : Result (betree.List T) :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
@@ -134,13 +149,15 @@ def betree.List.pop_front_back
   | betree.List.Cons x tl => Result.ret tl
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+   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 l => Result.ret hd
   | betree.List.Nil => Result.fail Error.panic
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+   Source: 'src/betree.rs', lines 327:4-327:44 -/
 def betree.ListTupleU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
@@ -148,7 +165,8 @@ def betree.ListTupleU64T.head_has_key
                              Result.ret (i = key)
   | betree.List.Nil => Result.ret false
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function -/
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+   Source: 'src/betree.rs', lines 339:4-339:73 -/
 divergent def betree.ListTupleU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
   Result ((betree.List (U64 × T)) × (betree.List (U64 × T)))
@@ -166,7 +184,8 @@ divergent def betree.ListTupleU64T.partition_at_pivot
         Result.ret (betree.List.Cons (i, t) l, ls1)
   | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+   Source: 'src/betree.rs', lines 359:4-364:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -186,7 +205,8 @@ def betree.Leaf.split
     let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
     Result.ret (st1, betree.Internal.mk self.id pivot n n0)
 
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2 -/
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
+   Source: 'src/betree.rs', lines 359:4-364:17 -/
 def betree.Leaf.split_back
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
@@ -203,7 +223,8 @@ def betree.Leaf.split_back
     let _ ← betree.store_leaf_node id1 content1 st0
     betree.NodeIdCounter.fresh_id_back node_id_cnt0
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+   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)) :
   Result (betree.List (U64 × betree.Message))
@@ -216,7 +237,8 @@ divergent def betree.Node.lookup_first_message_for_key
     else betree.Node.lookup_first_message_for_key key next_msgs
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
+   Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -234,7 +256,8 @@ divergent def betree.Node.lookup_first_message_for_key_back
         Result.ret (betree.List.Cons (i, m) next_msgs0)
   | betree.List.Nil => Result.ret ret0
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+   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)
   (st : State) :
@@ -264,7 +287,8 @@ divergent def betree.Node.apply_upserts
             betree.Message.Insert v)
         Result.ret (st0, v)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
+   Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts_back
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
@@ -292,7 +316,8 @@ divergent def betree.Node.apply_upserts_back
         betree.List.push_front (U64 × betree.Message) msgs (key,
           betree.Message.Insert v)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+   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) :=
   match bindings with
@@ -306,7 +331,8 @@ divergent def betree.Node.lookup_in_bindings
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ret none
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+   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))
@@ -316,7 +342,8 @@ mutual divergent def betree.Internal.lookup_in_children
   then betree.Node.lookup n key st
   else betree.Node.lookup n0 key st
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
+   Source: 'src/betree.rs', lines 395:4-395:63 -/
 divergent def betree.Internal.lookup_in_children_back
   (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
   let ⟨ i, i0, n, n0 ⟩ := self
@@ -330,7 +357,8 @@ divergent def betree.Internal.lookup_in_children_back
       let n1 ← betree.Node.lookup_back n0 key st
       Result.ret (betree.Internal.mk i i0 n n1)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+   Source: 'src/betree.rs', lines 709:4-709:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
   Result (State × (Option U64))
@@ -402,7 +430,8 @@ divergent def betree.Node.lookup
       let o ← betree.Node.lookup_in_bindings key bindings
       Result.ret (st0, o)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
+   Source: 'src/betree.rs', lines 709:4-709:58 -/
 divergent def betree.Node.lookup_back
   (self : betree.Node) (key : U64) (st : State) : Result betree.Node :=
   match self with
@@ -476,7 +505,8 @@ divergent def betree.Node.lookup_back
 end
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   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)) :
   Result (betree.List (U64 × betree.Message))
@@ -494,7 +524,8 @@ divergent def betree.Node.filter_messages_for_key
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+   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)) :
   Result (betree.List (U64 × betree.Message))
@@ -507,7 +538,8 @@ divergent def betree.Node.lookup_first_message_after_key
     else Result.ret (betree.List.Cons (k, m) next_msgs)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
+   Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
   (ret0 : betree.List (U64 × betree.Message)) :
@@ -526,7 +558,8 @@ divergent def betree.Node.lookup_first_message_after_key_back
   | betree.List.Nil => Result.ret ret0
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   Source: 'src/betree.rs', lines 521:4-521:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
   (new_msg : betree.Message) :
@@ -592,7 +625,8 @@ def betree.Node.apply_to_internal
         betree.Node.lookup_first_message_for_key_back key msgs msgs1
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   Source: 'src/betree.rs', lines 502:4-505:5 -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
   (new_msgs : betree.List (U64 × betree.Message)) :
@@ -606,7 +640,8 @@ divergent def betree.Node.apply_messages_to_internal
       betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+   Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) :
   Result (betree.List (U64 × U64))
@@ -619,7 +654,8 @@ divergent def betree.Node.lookup_mut_in_bindings
     else betree.Node.lookup_mut_in_bindings key tl
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
+   Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings_back
   (key : U64) (bindings : betree.List (U64 × U64))
   (ret0 : betree.List (U64 × U64)) :
@@ -637,7 +673,8 @@ divergent def betree.Node.lookup_mut_in_bindings_back
   | betree.List.Nil => Result.ret ret0
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   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)
   :
@@ -686,7 +723,8 @@ def betree.Node.apply_to_leaf
           betree.Node.lookup_mut_in_bindings_back key bindings bindings1
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ()) -/
+   (there is a single backward function, and the forward function returns ())
+   Source: 'src/betree.rs', lines 444:4-447:5 -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
   (new_msgs : betree.List (U64 × betree.Message)) :
@@ -700,7 +738,8 @@ divergent def betree.Node.apply_messages_to_leaf
       betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+   Source: 'src/betree.rs', lines 410:4-415:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -738,7 +777,8 @@ mutual divergent def betree.Internal.flush
           betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
         Result.ret (st0, msgs_left)
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: backward function 0
+   Source: 'src/betree.rs', lines 410:4-415:26 -/
 divergent def betree.Internal.flush_back
   (self : betree.Internal) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -772,7 +812,8 @@ divergent def betree.Internal.flush_back
           betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
         Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: forward function
+   Source: 'src/betree.rs', lines 588:4-593:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -820,7 +861,8 @@ divergent def betree.Node.apply_messages
           let (st1, _) ← betree.store_leaf_node node.id content0 st0
           Result.ret (st1, ())
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
+   Source: 'src/betree.rs', lines 588:4-593:5 -/
 divergent def betree.Node.apply_messages_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter)
@@ -874,7 +916,8 @@ divergent def betree.Node.apply_messages_back
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+   Source: 'src/betree.rs', lines 576:4-582:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -891,7 +934,8 @@ def betree.Node.apply
         (key, new_msg) l) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
+   Source: 'src/betree.rs', lines 576:4-582:5 -/
 def betree.Node.apply_back
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
@@ -902,7 +946,8 @@ def betree.Node.apply_back
   betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons
     (key, new_msg) l) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+   Source: 'src/betree.rs', lines 849:4-849:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
@@ -920,7 +965,8 @@ def betree.BeTree.new
         root := (betree.Node.Leaf { id := id, size := 0#u64 })
       })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+   Source: 'src/betree.rs', lines 868:4-868:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result (State × Unit)
@@ -932,7 +978,8 @@ def betree.BeTree.apply
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret (st0, ())
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
+   Source: 'src/betree.rs', lines 868:4-868:47 -/
 def betree.BeTree.apply_back
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
   Result betree.BeTree
@@ -942,7 +989,8 @@ def betree.BeTree.apply_back
       betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
     Result.ret { self with node_id_cnt := nic, root := n }
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+   Source: 'src/betree.rs', lines 874:4-874:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result (State × Unit)
@@ -954,14 +1002,16 @@ def betree.BeTree.insert
       betree.BeTree.apply_back self key (betree.Message.Insert value) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
+   Source: 'src/betree.rs', lines 874:4-874:52 -/
 def betree.BeTree.insert_back
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
   Result betree.BeTree
   :=
   betree.BeTree.apply_back self key (betree.Message.Insert value) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+   Source: 'src/betree.rs', lines 880:4-880:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) :=
   do
@@ -969,12 +1019,14 @@ def betree.BeTree.delete
     let _ ← betree.BeTree.apply_back self key betree.Message.Delete st
     Result.ret (st0, ())
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
+   Source: 'src/betree.rs', lines 880:4-880:38 -/
 def betree.BeTree.delete_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   betree.BeTree.apply_back self key betree.Message.Delete st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
+   Source: 'src/betree.rs', lines 886:4-886:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -986,7 +1038,8 @@ def betree.BeTree.upsert
     let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
     Result.ret (st0, ())
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
+   Source: 'src/betree.rs', lines 886:4-886:59 -/
 def betree.BeTree.upsert_back
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
@@ -994,21 +1047,24 @@ def betree.BeTree.upsert_back
   :=
   betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+   Source: 'src/betree.rs', lines 895:4-895:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
   betree.Node.lookup self.root key st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0 -/
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
+   Source: 'src/betree.rs', lines 895:4-895:62 -/
 def betree.BeTree.lookup_back
   (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   do
     let n ← betree.Node.lookup_back self.root key st
     Result.ret { self with root := n }
 
-/- [betree_main::main]: forward function -/
+/- [betree_main::main]: forward function
+   Source: 'src/betree_main.rs', lines 5:0-5:9 -/
 def main : Result Unit :=
   Result.ret ()
 
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index 1dc3af0e..95f88873 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -6,25 +6,30 @@ import BetreeMain.Types
 open Primitives
 open betree_main
 
-/- [betree_main::betree_utils::load_internal_node]: forward function -/
+/- [betree_main::betree_utils::load_internal_node]: forward function
+   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]: forward function -/
+/- [betree_main::betree_utils::store_internal_node]: forward function
+   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]: forward function -/
+/- [betree_main::betree_utils::load_leaf_node]: forward function
+   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]: forward function -/
+/- [betree_main::betree_utils::store_leaf_node]: forward function
+   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)
 
-/- [core::option::{core::option::Option<T>}::unwrap]: forward function -/
+/- [core::option::{core::option::Option<T>}::unwrap]: forward function
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)
 
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 2f5de6a0..6e528437 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -5,50 +5,59 @@ open Primitives
 
 namespace betree_main
 
-/- [betree_main::betree::List] -/
+/- [betree_main::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_main::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_main::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_main::betree::Leaf]
+   Source: 'src/betree.rs', lines 167:0-167:11 -/
 structure betree.Leaf where
   id : U64
   size : U64
 
 mutual
 
-/- [betree_main::betree::Internal] -/
+/- [betree_main::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_main::betree::Node]
+   Source: 'src/betree.rs', lines 179:0-179:9 -/
 inductive betree.Node :=
 | Internal : betree.Internal → betree.Node
 | Leaf : betree.Leaf → betree.Node
 
 end
 
-/- [betree_main::betree::Params] -/
+/- [betree_main::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_main::betree::NodeIdCounter]
+   Source: 'src/betree.rs', lines 201:0-201:20 -/
 structure betree.NodeIdCounter where
   next_node_id : U64
 
-/- [betree_main::betree::BeTree] -/
+/- [betree_main::betree::BeTree]
+   Source: 'src/betree.rs', lines 218:0-218:17 -/
 structure betree.BeTree where
   params : betree.Params
   node_id_cnt : betree.NodeIdCounter
-- 
cgit v1.2.3


From d84040e000333d6d2a212fb849a38fb73a65eb48 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 Nov 2023 17:41:42 +0100
Subject: Regenerate the files

---
 tests/lean/BetreeMain/Funs.lean | 42 ++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 45548884..4c862225 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -121,7 +121,7 @@ divergent def betree.List.split_at
         let (ls0, ls1) := p
         let l := ls0
         Result.ret (betree.List.Cons hd l, ls1)
-    | betree.List.Nil => Result.fail Error.panic
+    | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -138,7 +138,7 @@ def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret x
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
    Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -147,14 +147,14 @@ def betree.List.pop_front_back
   let ls := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
   | betree.List.Cons x tl => Result.ret tl
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
    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 l => Result.ret hd
-  | betree.List.Nil => Result.fail Error.panic
+  | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
    Source: 'src/betree.rs', lines 327:4-327:44 -/
@@ -241,20 +241,20 @@ divergent def betree.Node.lookup_first_message_for_key
    Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret0 : betree.List (U64 × betree.Message)) :
+  (ret : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
   match msgs with
   | betree.List.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
-    then Result.ret ret0
+    then Result.ret ret
     else
       do
         let next_msgs0 ←
-          betree.Node.lookup_first_message_for_key_back key next_msgs ret0
+          betree.Node.lookup_first_message_for_key_back key next_msgs ret
         Result.ret (betree.List.Cons (i, m) next_msgs0)
-  | betree.List.Nil => Result.ret ret0
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
    Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -271,8 +271,8 @@ divergent def betree.Node.apply_upserts
         let msg ← betree.List.pop_front (U64 × betree.Message) msgs
         let (_, m) := msg
         match m with
-        | betree.Message.Insert i => Result.fail Error.panic
-        | betree.Message.Delete => Result.fail Error.panic
+        | betree.Message.Insert i => Result.fail .panic
+        | betree.Message.Delete => Result.fail .panic
         | betree.Message.Upsert s =>
           do
             let v ← betree.upsert_update prev s
@@ -302,8 +302,8 @@ divergent def betree.Node.apply_upserts_back
         let msg ← betree.List.pop_front (U64 × betree.Message) msgs
         let (_, m) := msg
         match m with
-        | betree.Message.Insert i => Result.fail Error.panic
-        | betree.Message.Delete => Result.fail Error.panic
+        | betree.Message.Insert i => Result.fail .panic
+        | betree.Message.Delete => Result.fail .panic
         | betree.Message.Upsert s =>
           do
             let v ← betree.upsert_update prev s
@@ -542,7 +542,7 @@ divergent def betree.Node.lookup_first_message_after_key
    Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key_back
   (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret0 : betree.List (U64 × betree.Message)) :
+  (ret : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
   :=
   match msgs with
@@ -552,10 +552,10 @@ divergent def betree.Node.lookup_first_message_after_key_back
     then
       do
         let next_msgs0 ←
-          betree.Node.lookup_first_message_after_key_back key next_msgs ret0
+          betree.Node.lookup_first_message_after_key_back key next_msgs ret
         Result.ret (betree.List.Cons (k, m) next_msgs0)
-    else Result.ret ret0
-  | betree.List.Nil => Result.ret ret0
+    else Result.ret ret
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -658,19 +658,19 @@ divergent def betree.Node.lookup_mut_in_bindings
    Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings_back
   (key : U64) (bindings : betree.List (U64 × U64))
-  (ret0 : betree.List (U64 × U64)) :
+  (ret : betree.List (U64 × U64)) :
   Result (betree.List (U64 × U64))
   :=
   match bindings with
   | betree.List.Cons hd tl =>
     let (i, i0) := hd
     if i >= key
-    then Result.ret ret0
+    then Result.ret ret
     else
       do
-        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret
         Result.ret (betree.List.Cons (i, i0) tl0)
-  | betree.List.Nil => Result.ret ret0
+  | betree.List.Nil => Result.ret ret
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
    (there is a single backward function, and the forward function returns ())
@@ -1069,6 +1069,6 @@ def main : Result Unit :=
   Result.ret ()
 
 /- Unit test for [betree_main::main] -/
-#assert (main == .ret ())
+#assert (main == Result.ret ())
 
 end betree_main
-- 
cgit v1.2.3


From bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 10:29:25 +0100
Subject: Generate a dedicated file for the external types

---
 tests/lean/BetreeMain/Types.lean                  | 4 +---
 tests/lean/BetreeMain/TypesExternal.lean          | 7 +++++++
 tests/lean/BetreeMain/TypesExternal_Template.lean | 9 +++++++++
 3 files changed, 17 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/BetreeMain/TypesExternal.lean
 create mode 100644 tests/lean/BetreeMain/TypesExternal_Template.lean

(limited to 'tests/lean/BetreeMain')

diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 6e528437..877508f6 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [betree_main]: type definitions
 import Base
+import BetreeMain.TypesExternal
 open Primitives
 
 namespace betree_main
@@ -63,7 +64,4 @@ structure betree.BeTree where
   node_id_cnt : betree.NodeIdCounter
   root : betree.Node
 
-/- The state type used in the state-error monad -/
-axiom State : Type
-
 end betree_main
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean
new file mode 100644
index 00000000..1701eaaf
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [betree_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..bbac7e99
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
-- 
cgit v1.2.3