Regenerate the Lean test files

22 files changed, 275 insertions, 192 deletions

diff --git a/tests/lean/BetreeMain/ExternalFuns.lean b/tests/lean/BetreeMain/ExternalFuns.lean
new file mode 100644
index 00000000..59beb514
--- /dev/null
+++ b/tests/lean/BetreeMain/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import BetreeMain.Types
+import BetreeMain.Opaque
+
+namespace BetreeMain
+
+def opaque_defs : OpaqueDefs := by sorry
+
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index fb48b3a6..2eb7fa1f 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -5,6 +5,8 @@ import BetreeMain.Types
 import BetreeMain.ExternalFuns
 open Primitives
 
+namespace BetreeMain
+
 /- [betree_main::betree::load_internal_node] -/
 def betree_load_internal_node_fwd
   (id : U64) (st : State) :
@@ -75,13 +77,13 @@ def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
 /- [betree_main::betree::upsert_update] -/
 def betree_upsert_update_fwd
   (prev : Option U64) (st : betree_upsert_fun_state_t) : Result U64 :=
-  match h: prev with
+  match prev with
   | Option.none =>
-    match h: st with
+    match st with
     | betree_upsert_fun_state_t.Add v => Result.ret v
     | betree_upsert_fun_state_t.Sub i => Result.ret (U64.ofInt 0 (by intlit))
   | Option.some prev0 =>
-    match h: st with
+    match st with
     | betree_upsert_fun_state_t.Add v =>
       do
         let margin ← core_num_u64_max_c - prev0
@@ -96,7 +98,7 @@ def betree_upsert_update_fwd
 /- [betree_main::betree::List::{1}::len] -/
 divergent def betree_list_len_fwd
   (T : Type) (self : betree_list_t T) : Result U64 :=
-  match h: self with
+  match self with
   | betree_list_t.Cons t tl =>
     do
       let i ← betree_list_len_fwd T tl
@@ -111,7 +113,7 @@ divergent def betree_list_split_at_fwd
   if n = (U64.ofInt 0 (by intlit))
   then Result.ret (betree_list_t.Nil, self)
   else
-    match h: self with
+    match self with
     | betree_list_t.Cons hd tl =>
       do
         let i ← n - (U64.ofInt 1 (by intlit))
@@ -131,7 +133,7 @@ def betree_list_push_front_fwd_back
 /- [betree_main::betree::List::{1}::pop_front] -/
 def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
   let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
-  match h: ls with
+  match ls with
   | betree_list_t.Cons x tl => Result.ret x
   | betree_list_t.Nil => Result.fail Error.panic
 
@@ -139,20 +141,20 @@ def betree_list_pop_front_fwd (T : Type) (self : betree_list_t T) : Result T :=
 def betree_list_pop_front_back
   (T : Type) (self : betree_list_t T) : Result (betree_list_t T) :=
   let ls := mem_replace_fwd (betree_list_t T) self betree_list_t.Nil
-  match h: ls with
+  match ls with
   | betree_list_t.Cons x tl => Result.ret tl
   | betree_list_t.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::List::{1}::hd] -/
 def betree_list_hd_fwd (T : Type) (self : betree_list_t T) : Result T :=
-  match h: self with
+  match self with
   | betree_list_t.Cons hd l => Result.ret hd
   | betree_list_t.Nil => Result.fail Error.panic
 
 /- [betree_main::betree::List::{2}::head_has_key] -/
 def betree_list_head_has_key_fwd
   (T : Type) (self : betree_list_t (U64 × T)) (key : U64) : Result Bool :=
-  match h: self with
+  match self with
   | betree_list_t.Cons hd l => let (i, _) := hd
                                Result.ret (i = key)
   | betree_list_t.Nil => Result.ret false
@@ -162,7 +164,7 @@ divergent def betree_list_partition_at_pivot_fwd
   (T : Type) (self : betree_list_t (U64 × T)) (pivot : U64) :
   Result ((betree_list_t (U64 × T)) × (betree_list_t (U64 × T)))
   :=
-  match h: self with
+  match self with
   | betree_list_t.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
@@ -204,7 +206,7 @@ def betree_leaf_split_fwd
         betree_leaf_id := id1,
         betree_leaf_size := params.betree_params_split_size
       }
-    Result.ret (st1, mkbetree_internal_t self.betree_leaf_id pivot n n0)
+    Result.ret (st1, betree_internal_t.mk self.betree_leaf_id pivot n n0)
 
 /- [betree_main::betree::Leaf::{3}::split] -/
 def betree_leaf_split_back
@@ -229,7 +231,7 @@ def betree_leaf_split_back
 /- [betree_main::betree::Node::{5}::lookup_in_bindings] -/
 divergent def betree_node_lookup_in_bindings_fwd
   (key : U64) (bindings : betree_list_t (U64 × U64)) : Result (Option U64) :=
-  match h: bindings with
+  match bindings with
   | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if i = key
@@ -245,7 +247,7 @@ divergent def betree_node_lookup_first_message_for_key_fwd
   (key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: msgs with
+  match msgs with
   | betree_list_t.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
@@ -259,7 +261,7 @@ divergent def betree_node_lookup_first_message_for_key_back
   (ret0 : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: msgs with
+  match msgs with
   | betree_list_t.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
@@ -284,7 +286,7 @@ divergent def betree_node_apply_upserts_fwd
       do
         let msg ← betree_list_pop_front_fwd (U64 × betree_message_t) msgs
         let (_, m) := msg
-        match h: m with
+        match m with
         | betree_message_t.Insert i => Result.fail Error.panic
         | betree_message_t.Delete => Result.fail Error.panic
         | betree_message_t.Upsert s =>
@@ -314,7 +316,7 @@ divergent def betree_node_apply_upserts_back
       do
         let msg ← betree_list_pop_front_fwd (U64 × betree_message_t) msgs
         let (_, m) := msg
-        match h: m with
+        match m with
         | betree_message_t.Insert i => Result.fail Error.panic
         | betree_message_t.Delete => Result.fail Error.panic
         | betree_message_t.Upsert s =>
@@ -334,27 +336,27 @@ mutual divergent def betree_node_lookup_fwd
   (self : betree_node_t) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
-  match h: self with
+  match self with
   | betree_node_t.Internal node =>
     do
-      let (mkbetree_internal_t i i0 n n0) := node
+      let ⟨ i, i0, n, n0 ⟩ := node
       let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
-      match h: pending with
+      match pending with
       | betree_list_t.Cons p l =>
         let (k, msg) := p
         if k != key
         then
           do
             let (st1, opt) ←
-              betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0
+              betree_internal_lookup_in_children_fwd (betree_internal_t.mk i i0
                 n n0) key st0
             let _ ←
               betree_node_lookup_first_message_for_key_back key msgs
                 (betree_list_t.Cons (k, msg) l)
             Result.ret (st1, opt)
         else
-          match h: msg with
+          match msg with
           | betree_message_t.Insert v =>
             do
               let _ ←
@@ -370,15 +372,15 @@ mutual divergent def betree_node_lookup_fwd
           | betree_message_t.Upsert ufs =>
             do
               let (st1, v) ←
-                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+                betree_internal_lookup_in_children_fwd (betree_internal_t.mk i
                   i0 n n0) key st0
               let (st2, v0) ←
                 betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
                   betree_message_t.Upsert ufs) l) v key st1
               let node0 ←
-                betree_internal_lookup_in_children_back (mkbetree_internal_t i
+                betree_internal_lookup_in_children_back (betree_internal_t.mk i
                   i0 n n0) key st0
-              let (mkbetree_internal_t i1 _ _ _) := node0
+              let ⟨ i1, _, _, _ ⟩ := node0
               let pending0 ←
                 betree_node_apply_upserts_back (betree_list_t.Cons (k,
                   betree_message_t.Upsert ufs) l) v key st1
@@ -389,7 +391,7 @@ mutual divergent def betree_node_lookup_fwd
       | betree_list_t.Nil =>
         do
           let (st1, opt) ←
-            betree_internal_lookup_in_children_fwd (mkbetree_internal_t i i0 n
+            betree_internal_lookup_in_children_fwd (betree_internal_t.mk i i0 n
               n0) key st0
           let _ ←
             betree_node_lookup_first_message_for_key_back key msgs
@@ -404,13 +406,13 @@ mutual divergent def betree_node_lookup_fwd
 /- [betree_main::betree::Node::{5}::lookup] -/
 divergent def betree_node_lookup_back
   (self : betree_node_t) (key : U64) (st : State) : Result betree_node_t :=
-  match h: self with
+  match self with
   | betree_node_t.Internal node =>
     do
-      let (mkbetree_internal_t i i0 n n0) := node
+      let ⟨ i, i0, n, n0 ⟩ := node
       let (st0, msgs) ← betree_load_internal_node_fwd i st
       let pending ← betree_node_lookup_first_message_for_key_fwd key msgs
-      match h: pending with
+      match pending with
       | betree_list_t.Cons p l =>
         let (k, msg) := p
         if k != key
@@ -420,44 +422,44 @@ divergent def betree_node_lookup_back
               betree_node_lookup_first_message_for_key_back key msgs
                 (betree_list_t.Cons (k, msg) l)
             let node0 ←
-              betree_internal_lookup_in_children_back (mkbetree_internal_t i i0
-                n n0) key st0
+              betree_internal_lookup_in_children_back (betree_internal_t.mk i
+                i0 n n0) key st0
             Result.ret (betree_node_t.Internal node0)
         else
-          match h: msg with
+          match msg with
           | betree_message_t.Insert v =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
                   (betree_list_t.Cons (k, betree_message_t.Insert v) l)
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+              Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n
                 n0))
           | betree_message_t.Delete =>
             do
               let _ ←
                 betree_node_lookup_first_message_for_key_back key msgs
                   (betree_list_t.Cons (k, betree_message_t.Delete) l)
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n
+              Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n
                 n0))
           | betree_message_t.Upsert ufs =>
             do
               let (st1, v) ←
-                betree_internal_lookup_in_children_fwd (mkbetree_internal_t i
+                betree_internal_lookup_in_children_fwd (betree_internal_t.mk i
                   i0 n n0) key st0
               let (st2, _) ←
                 betree_node_apply_upserts_fwd (betree_list_t.Cons (k,
                   betree_message_t.Upsert ufs) l) v key st1
               let node0 ←
-                betree_internal_lookup_in_children_back (mkbetree_internal_t i
+                betree_internal_lookup_in_children_back (betree_internal_t.mk i
                   i0 n n0) key st0
-              let (mkbetree_internal_t i1 i2 n1 n2) := node0
+              let ⟨ i1, i2, n1, n2 ⟩ := node0
               let pending0 ←
                 betree_node_apply_upserts_back (betree_list_t.Cons (k,
                   betree_message_t.Upsert ufs) l) v key st1
               let msgs0 ←
                 betree_node_lookup_first_message_for_key_back key msgs pending0
               let _ ← betree_store_internal_node_fwd i1 msgs0 st2
-              Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1
+              Result.ret (betree_node_t.Internal (betree_internal_t.mk i1 i2 n1
                 n2))
       | betree_list_t.Nil =>
         do
@@ -465,8 +467,8 @@ divergent def betree_node_lookup_back
             betree_node_lookup_first_message_for_key_back key msgs
               betree_list_t.Nil
           let node0 ←
-            betree_internal_lookup_in_children_back (mkbetree_internal_t i i0 n
-              n0) key st0
+            betree_internal_lookup_in_children_back (betree_internal_t.mk i i0
+              n n0) key st0
           Result.ret (betree_node_t.Internal node0)
   | betree_node_t.Leaf node =>
     do
@@ -479,7 +481,7 @@ divergent def betree_internal_lookup_in_children_fwd
   (self : betree_internal_t) (key : U64) (st : State) :
   Result (State × (Option U64))
   :=
-  let (mkbetree_internal_t _ i n n0) := self
+  let ⟨ _, i, n, n0 ⟩ := self
   if key < i
   then betree_node_lookup_fwd n key st
   else betree_node_lookup_fwd n0 key st
@@ -489,16 +491,16 @@ divergent def betree_internal_lookup_in_children_back
   (self : betree_internal_t) (key : U64) (st : State) :
   Result betree_internal_t
   :=
-  let (mkbetree_internal_t i i0 n n0) := self
+  let ⟨ i, i0, n, n0 ⟩ := self
   if key < i0
   then
     do
       let n1 ← betree_node_lookup_back n key st
-      Result.ret (mkbetree_internal_t i i0 n1 n0)
+      Result.ret (betree_internal_t.mk i i0 n1 n0)
   else
     do
       let n1 ← betree_node_lookup_back n0 key st
-      Result.ret (mkbetree_internal_t i i0 n n1)
+      Result.ret (betree_internal_t.mk i i0 n n1)
 
 end
 
@@ -507,7 +509,7 @@ divergent def betree_node_lookup_mut_in_bindings_fwd
   (key : U64) (bindings : betree_list_t (U64 × U64)) :
   Result (betree_list_t (U64 × U64))
   :=
-  match h: bindings with
+  match bindings with
   | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if i >= key
@@ -521,7 +523,7 @@ divergent def betree_node_lookup_mut_in_bindings_back
   (ret0 : betree_list_t (U64 × U64)) :
   Result (betree_list_t (U64 × U64))
   :=
-  match h: bindings with
+  match bindings with
   | betree_list_t.Cons hd tl =>
     let (i, i0) := hd
     if i >= key
@@ -545,7 +547,7 @@ def betree_node_apply_to_leaf_fwd_back
     then
       do
         let hd ← betree_list_pop_front_fwd (U64 × U64) bindings0
-        match h: new_msg with
+        match new_msg with
         | betree_message_t.Insert v =>
           do
             let bindings1 ← betree_list_pop_front_back (U64 × U64) bindings0
@@ -565,7 +567,7 @@ def betree_node_apply_to_leaf_fwd_back
               betree_list_push_front_fwd_back (U64 × U64) bindings1 (key, v)
             betree_node_lookup_mut_in_bindings_back key bindings bindings2
     else
-      match h: new_msg with
+      match new_msg with
       | betree_message_t.Insert v =>
         do
           let bindings1 ←
@@ -586,7 +588,7 @@ divergent def betree_node_apply_messages_to_leaf_fwd_back
   (new_msgs : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × U64))
   :=
-  match h: new_msgs with
+  match new_msgs with
   | betree_list_t.Cons new_msg new_msgs_tl =>
     do
       let (i, m) := new_msg
@@ -599,7 +601,7 @@ divergent def betree_node_filter_messages_for_key_fwd_back
   (key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: msgs with
+  match msgs with
   | betree_list_t.Cons p l =>
     let (k, m) := p
     if k = key
@@ -617,7 +619,7 @@ divergent def betree_node_lookup_first_message_after_key_fwd
   (key : U64) (msgs : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: msgs with
+  match msgs with
   | betree_list_t.Cons p next_msgs =>
     let (k, m) := p
     if k = key
@@ -631,7 +633,7 @@ divergent def betree_node_lookup_first_message_after_key_back
   (ret0 : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: msgs with
+  match msgs with
   | betree_list_t.Cons p next_msgs =>
     let (k, m) := p
     if k = key
@@ -654,7 +656,7 @@ def betree_node_apply_to_internal_fwd_back
     let b ← betree_list_head_has_key_fwd betree_message_t msgs0 key
     if b
     then
-      match h: new_msg with
+      match new_msg with
       | betree_message_t.Insert i =>
         do
           let msgs1 ← betree_node_filter_messages_for_key_fwd_back key msgs0
@@ -673,7 +675,7 @@ def betree_node_apply_to_internal_fwd_back
         do
           let p ← betree_list_hd_fwd (U64 × betree_message_t) msgs0
           let (_, m) := p
-          match h: m with
+          match m with
           | betree_message_t.Insert prev =>
             do
               let v ← betree_upsert_update_fwd (Option.some prev) s
@@ -715,7 +717,7 @@ divergent def betree_node_apply_messages_to_internal_fwd_back
   (new_msgs : betree_list_t (U64 × betree_message_t)) :
   Result (betree_list_t (U64 × betree_message_t))
   :=
-  match h: new_msgs with
+  match new_msgs with
   | betree_list_t.Cons new_msg new_msgs_tl =>
     do
       let (i, m) := new_msg
@@ -730,10 +732,10 @@ mutual divergent def betree_node_apply_messages_fwd
   (msgs : betree_list_t (U64 × betree_message_t)) (st : State) :
   Result (State × Unit)
   :=
-  match h: self with
+  match self with
   | betree_node_t.Internal node =>
     do
-      let (mkbetree_internal_t i i0 n n0) := node
+      let ⟨ i, i0, n, n0 ⟩ := node
       let (st0, content) ← betree_load_internal_node_fwd i st
       let content0 ←
         betree_node_apply_messages_to_internal_fwd_back content msgs
@@ -742,12 +744,12 @@ mutual divergent def betree_node_apply_messages_fwd
       then
         do
           let (st1, content1) ←
-            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+            betree_internal_flush_fwd (betree_internal_t.mk i i0 n n0) params
               node_id_cnt content0 st0
           let (node0, _) ←
-            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+            betree_internal_flush_back (betree_internal_t.mk i i0 n n0) params
               node_id_cnt content0 st0
-          let (mkbetree_internal_t i1 _ _ _) := node0
+          let ⟨ i1, _, _, _ ⟩ := node0
           let (st2, _) ← betree_store_internal_node_fwd i1 content1 st1
           Result.ret (st2, ())
       else
@@ -782,10 +784,10 @@ divergent def betree_node_apply_messages_back
   (msgs : betree_list_t (U64 × betree_message_t)) (st : State) :
   Result (betree_node_t × betree_node_id_counter_t)
   :=
-  match h: self with
+  match self with
   | betree_node_t.Internal node =>
     do
-      let (mkbetree_internal_t i i0 n n0) := node
+      let ⟨ i, i0, n, n0 ⟩ := node
       let (st0, content) ← betree_load_internal_node_fwd i st
       let content0 ←
         betree_node_apply_messages_to_internal_fwd_back content msgs
@@ -794,19 +796,19 @@ divergent def betree_node_apply_messages_back
       then
         do
           let (st1, content1) ←
-            betree_internal_flush_fwd (mkbetree_internal_t i i0 n n0) params
+            betree_internal_flush_fwd (betree_internal_t.mk i i0 n n0) params
               node_id_cnt content0 st0
           let (node0, node_id_cnt0) ←
-            betree_internal_flush_back (mkbetree_internal_t i i0 n n0) params
+            betree_internal_flush_back (betree_internal_t.mk i i0 n n0) params
               node_id_cnt content0 st0
-          let (mkbetree_internal_t i1 i2 n1 n2) := node0
+          let ⟨ i1, i2, n1, n2 ⟩ := node0
           let _ ← betree_store_internal_node_fwd i1 content1 st1
-          Result.ret (betree_node_t.Internal (mkbetree_internal_t i1 i2 n1 n2),
-            node_id_cnt0)
+          Result.ret (betree_node_t.Internal (betree_internal_t.mk i1 i2 n1
+            n2), node_id_cnt0)
       else
         do
           let _ ← betree_store_internal_node_fwd i content0 st0
-          Result.ret (betree_node_t.Internal (mkbetree_internal_t i i0 n n0),
+          Result.ret (betree_node_t.Internal (betree_internal_t.mk i i0 n n0),
             node_id_cnt)
   | betree_node_t.Leaf node =>
     do
@@ -839,7 +841,7 @@ divergent def betree_internal_flush_fwd
   Result (State × (betree_list_t (U64 × betree_message_t)))
   :=
   do
-    let (mkbetree_internal_t _ i n n0) := self
+    let ⟨ _, i, n, n0 ⟩ := self
     let p ← betree_list_partition_at_pivot_fwd betree_message_t content i
     let (msgs_left, msgs_right) := p
     let len_left ← betree_list_len_fwd (U64 × betree_message_t) msgs_left
@@ -879,7 +881,7 @@ divergent def betree_internal_flush_back
   Result (betree_internal_t × betree_node_id_counter_t)
   :=
   do
-    let (mkbetree_internal_t i i0 n n0) := self
+    let ⟨ i, i0, n, n0 ⟩ := self
     let p ← betree_list_partition_at_pivot_fwd betree_message_t content i0
     let (msgs_left, msgs_right) := p
     let len_left ← betree_list_len_fwd (U64 × betree_message_t) msgs_left
@@ -898,13 +900,13 @@ divergent def betree_internal_flush_back
             let (n2, node_id_cnt1) ←
               betree_node_apply_messages_back n0 params node_id_cnt0 msgs_right
                 st0
-            Result.ret (mkbetree_internal_t i i0 n1 n2, node_id_cnt1)
-        else Result.ret (mkbetree_internal_t i i0 n1 n0, node_id_cnt0)
+            Result.ret (betree_internal_t.mk i i0 n1 n2, node_id_cnt1)
+        else Result.ret (betree_internal_t.mk i i0 n1 n0, node_id_cnt0)
     else
       do
         let (n1, node_id_cnt0) ←
           betree_node_apply_messages_back n0 params node_id_cnt msgs_right st
-        Result.ret (mkbetree_internal_t i i0 n n1, node_id_cnt0)
+        Result.ret (betree_internal_t.mk i i0 n n1, node_id_cnt0)
 
 end
 
@@ -1069,3 +1071,4 @@ def main_fwd : Result Unit :=
 /- Unit test for [betree_main::main] -/
 #assert (main_fwd == .ret ())
 
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Opaque.lean b/tests/lean/BetreeMain/Opaque.lean
index c8226d4e..d043186b 100644
--- a/tests/lean/BetreeMain/Opaque.lean
+++ b/tests/lean/BetreeMain/Opaque.lean
@@ -4,28 +4,32 @@ import Base
 import BetreeMain.Types
 open Primitives
 
+namespace BetreeMain
+
 structure OpaqueDefs where
   
   /- [betree_main::betree_utils::load_internal_node] -/
   betree_utils_load_internal_node_fwd
     :
-    U64 -> State -> Result (State × (betree_list_t (U64 × betree_message_t)))
+    U64 → State → Result (State × (betree_list_t (U64 ×
+      betree_message_t)))
   
   /- [betree_main::betree_utils::store_internal_node] -/
   betree_utils_store_internal_node_fwd
     :
-    U64 -> betree_list_t (U64 × betree_message_t) -> State -> Result (State ×
-      Unit)
+    U64 → betree_list_t (U64 × betree_message_t) → State → Result (State
+      × Unit)
   
   /- [betree_main::betree_utils::load_leaf_node] -/
   betree_utils_load_leaf_node_fwd
-    : U64 -> State -> Result (State × (betree_list_t (U64 × U64)))
+    : U64 → State → Result (State × (betree_list_t (U64 × U64)))
   
   /- [betree_main::betree_utils::store_leaf_node] -/
   betree_utils_store_leaf_node_fwd
-    : U64 -> betree_list_t (U64 × U64) -> State -> Result (State × Unit)
+    : U64 → betree_list_t (U64 × U64) → State → Result (State × Unit)
   
   /- [core::option::Option::{0}::unwrap] -/
   core_option_option_unwrap_fwd
-    (T : Type) : Option T -> State -> Result (State × T)
+    (T : Type) : Option T → State → Result (State × T)
   
+end BetreeMain
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 4875a8ba..cfed6a28 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -3,21 +3,23 @@
 import Base
 open Primitives
 
+namespace BetreeMain
+
 /- [betree_main::betree::List] -/
 inductive betree_list_t (T : Type) :=
-| Cons : T -> betree_list_t T -> betree_list_t T
+| Cons : T → betree_list_t T → betree_list_t T
 | Nil : betree_list_t T
 
 /- [betree_main::betree::UpsertFunState] -/
 inductive betree_upsert_fun_state_t :=
-| Add : U64 -> betree_upsert_fun_state_t
-| Sub : U64 -> betree_upsert_fun_state_t
+| Add : U64 → betree_upsert_fun_state_t
+| Sub : U64 → betree_upsert_fun_state_t
 
 /- [betree_main::betree::Message] -/
 inductive betree_message_t :=
-| Insert : U64 -> betree_message_t
+| Insert : U64 → betree_message_t
 | Delete : betree_message_t
-| Upsert : betree_upsert_fun_state_t -> betree_message_t
+| Upsert : betree_upsert_fun_state_t → betree_message_t
 
 /- [betree_main::betree::Leaf] -/
 structure betree_leaf_t where
@@ -28,17 +30,12 @@ mutual
 
 /- [betree_main::betree::Node] -/
 inductive betree_node_t :=
-| Internal : betree_internal_t -> betree_node_t
-| Leaf : betree_leaf_t -> betree_node_t
+| Internal : betree_internal_t → betree_node_t
+| Leaf : betree_leaf_t → betree_node_t
 
 /- [betree_main::betree::Internal] -/
 inductive betree_internal_t :=
-| mkbetree_internal_t :
-  U64 ->
-  U64 ->
-  betree_node_t ->
-  betree_node_t ->
-  betree_internal_t
+| mk : U64 → U64 → betree_node_t → betree_node_t → betree_internal_t
 
 end
 
@@ -60,3 +57,4 @@ structure betree_be_tree_t where
 /- The state type used in the state-error monad -/
 axiom State : Type
 
+end BetreeMain
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index cd2f88f5..9f6a47de 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -3,6 +3,8 @@
 import Base
 open Primitives
 
+namespace Constants
+
 /- [constants::X0] -/
 def x0_body : Result U32 := Result.ret (U32.ofInt 0 (by intlit))
 def x0_c : U32 := eval_global x0_body (by simp)
@@ -130,3 +132,4 @@ def s4_body : Result (pair_t U32 U32) :=
   mk_pair1_fwd (U32.ofInt 7 (by intlit)) (U32.ofInt 8 (by intlit))
 def s4_c : pair_t U32 U32 := eval_global s4_body (by simp)
 
+end Constants
diff --git a/tests/lean/External/ExternalFuns.lean b/tests/lean/External/ExternalFuns.lean
new file mode 100644
index 00000000..d63db2ac
--- /dev/null
+++ b/tests/lean/External/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import External.Types
+import External.Opaque
+
+namespace External
+
+def opaque_defs : OpaqueDefs := sorry
+
+end External
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 73e45938..e36987e0 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -5,6 +5,8 @@ import External.Types
 import External.ExternalFuns
 open Primitives
 
+namespace External
+
 /- [external::swap] -/
 def swap_fwd
   (T : Type) (x : T) (y : T) (st : State) : Result (State × Unit) :=
@@ -86,3 +88,4 @@ def test_swap_non_zero_fwd (x : U32) (st : State) : Result (State × U32) :=
     then Result.fail Error.panic
     else Result.ret (st1, x0)
 
+end External
diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean
index 5483c3a9..1c0db095 100644
--- a/tests/lean/External/Opaque.lean
+++ b/tests/lean/External/Opaque.lean
@@ -4,25 +4,29 @@ import Base
 import External.Types
 open Primitives
 
+namespace External
+
 structure OpaqueDefs where
   
   /- [core::mem::swap] -/
-  core_mem_swap_fwd (T : Type) : T -> T -> State -> Result (State × Unit)
+  core_mem_swap_fwd (T : Type) : T → T → State → Result (State × Unit)
   
   /- [core::mem::swap] -/
   core_mem_swap_back0
-    (T : Type) : T -> T -> State -> State -> Result (State × T)
+    (T : Type) : T → T → State → State → Result (State × T)
   
   /- [core::mem::swap] -/
   core_mem_swap_back1
-    (T : Type) : T -> T -> State -> State -> Result (State × T)
+    (T : Type) : T → T → State → State → Result (State × T)
   
   /- [core::num::nonzero::NonZeroU32::{14}::new] -/
   core_num_nonzero_non_zero_u32_new_fwd
     :
-    U32 -> State -> Result (State × (Option core_num_nonzero_non_zero_u32_t))
+    U32 → State → Result (State × (Option
+      core_num_nonzero_non_zero_u32_t))
   
   /- [core::option::Option::{0}::unwrap] -/
   core_option_option_unwrap_fwd
-    (T : Type) : Option T -> State -> Result (State × T)
+    (T : Type) : Option T → State → Result (State × T)
   
+end External
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 25907da2..fda0670e 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -3,9 +3,12 @@
 import Base
 open Primitives
 
+namespace External
+
 /- [core::num::nonzero::NonZeroU32] -/
 axiom core_num_nonzero_non_zero_u32_t : Type
 
 /- The state type used in the state-error monad -/
 axiom State : Type
 
+end External
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 26742d5d..b4254726 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -4,6 +4,8 @@ import Base
 import Hashmap.Types
 open Primitives
 
+namespace Hashmap
+
 /- [hashmap::hash_key] -/
 def hash_key_fwd (k : Usize) : Result Usize :=
   Result.ret k
@@ -82,7 +84,7 @@ def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize :=
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 divergent def hash_map_insert_in_list_loop_fwd
   (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret false
@@ -97,7 +99,7 @@ def hash_map_insert_in_list_fwd
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 divergent def hash_map_insert_in_list_loop_back
   (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret (list_t.Cons ckey value tl)
@@ -146,7 +148,7 @@ def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
 /- [hashmap::HashMap::{0}::move_elements_from_list] -/
 divergent def hash_map_move_elements_from_list_loop_fwd_back
   (T : Type) (ntable : hash_map_t T) (ls : list_t T) : Result (hash_map_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons k v tl =>
     do
       let ntable0 ← hash_map_insert_no_resize_fwd_back T ntable k v
@@ -224,7 +226,7 @@ def hash_map_insert_fwd_back
 /- [hashmap::HashMap::{0}::contains_key_in_list] -/
 divergent def hash_map_contains_key_in_list_loop_fwd
   (T : Type) (key : Usize) (ls : list_t T) : Result Bool :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey t tl =>
     if ckey = key
     then Result.ret true
@@ -249,7 +251,7 @@ def hash_map_contains_key_fwd
 /- [hashmap::HashMap::{0}::get_in_list] -/
 divergent def hash_map_get_in_list_loop_fwd
   (T : Type) (key : Usize) (ls : list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret cvalue
@@ -274,7 +276,7 @@ def hash_map_get_fwd
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 divergent def hash_map_get_mut_in_list_loop_fwd
   (T : Type) (ls : list_t T) (key : Usize) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret cvalue
@@ -289,7 +291,7 @@ def hash_map_get_mut_in_list_fwd
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 divergent def hash_map_get_mut_in_list_loop_back
   (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret (list_t.Cons ckey ret0 tl)
@@ -331,13 +333,13 @@ def hash_map_get_mut_back
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 divergent def hash_map_remove_from_list_loop_fwd
   (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey t tl =>
     if ckey = key
     then
       let mv_ls :=
         mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
-      match h: mv_ls with
+      match mv_ls with
       | list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
       | list_t.Nil => Result.fail Error.panic
     else hash_map_remove_from_list_loop_fwd T key tl
@@ -351,13 +353,13 @@ def hash_map_remove_from_list_fwd
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 divergent def hash_map_remove_from_list_loop_back
   (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons ckey t tl =>
     if ckey = key
     then
       let mv_ls :=
         mem_replace_fwd (list_t T) (list_t.Cons ckey t tl) list_t.Nil
-      match h: mv_ls with
+      match mv_ls with
       | list_t.Cons i cvalue tl0 => Result.ret tl0
       | list_t.Nil => Result.fail Error.panic
     else
@@ -380,7 +382,7 @@ def hash_map_remove_fwd
     let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let x ← hash_map_remove_from_list_fwd T key l
-    match h: x with
+    match x with
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
@@ -396,7 +398,7 @@ def hash_map_remove_back
     let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let x ← hash_map_remove_from_list_fwd T key l
-    match h: x with
+    match x with
     | Option.none =>
       do
         let l0 ← hash_map_remove_from_list_back T key l
@@ -441,7 +443,7 @@ def test1_fwd : Result Unit :=
           do
             let x ←
               hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit))
-            match h: x with
+            match x with
             | Option.none => Result.fail Error.panic
             | Option.some x0 =>
               if not (x0 = (U64.ofInt 56 (by intlit)))
@@ -472,3 +474,4 @@ def test1_fwd : Result Unit :=
 /- Unit test for [hashmap::test1] -/
 #assert (test1_fwd == .ret ())
 
+end Hashmap
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index af26f363..0aec6acf 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -3,9 +3,11 @@
 import Base
 open Primitives
 
+namespace Hashmap
+
 /- [hashmap::List] -/
 inductive list_t (T : Type) :=
-| Cons : Usize -> T -> list_t T -> list_t T
+| Cons : Usize → T → list_t T → list_t T
 | Nil : list_t T
 
 /- [hashmap::HashMap] -/
@@ -15,3 +17,4 @@ structure hash_map_t (T : Type) where
   hash_map_max_load : Usize
   hash_map_slots : Vec (list_t T)
 
+end Hashmap
diff --git a/tests/lean/HashmapMain/ExternalFuns.lean b/tests/lean/HashmapMain/ExternalFuns.lean
new file mode 100644
index 00000000..bc831158
--- /dev/null
+++ b/tests/lean/HashmapMain/ExternalFuns.lean
@@ -0,0 +1,9 @@
+import Base
+import HashmapMain.Types
+import HashmapMain.Opaque
+
+namespace HashmapMain
+
+def opaque_defs : OpaqueDefs := by sorry
+
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index a59a9f26..34a0eca1 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -5,6 +5,8 @@ import HashmapMain.Types
 import HashmapMain.ExternalFuns
 open Primitives
 
+namespace HashmapMain
+
 /- [hashmap_main::hashmap::hash_key] -/
 def hashmap_hash_key_fwd (k : Usize) : Result Usize :=
   Result.ret k
@@ -92,7 +94,7 @@ def hashmap_hash_map_len_fwd
 /- [hashmap_main::hashmap::HashMap::{0}::insert_in_list] -/
 divergent def hashmap_hash_map_insert_in_list_loop_fwd
   (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) : Result Bool :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret false
@@ -109,7 +111,7 @@ divergent def hashmap_hash_map_insert_in_list_loop_back
   (T : Type) (key : Usize) (value : T) (ls : hashmap_list_t T) :
   Result (hashmap_list_t T)
   :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret (hashmap_list_t.Cons ckey value tl)
@@ -173,7 +175,7 @@ divergent def hashmap_hash_map_move_elements_from_list_loop_fwd_back
   (T : Type) (ntable : hashmap_hash_map_t T) (ls : hashmap_list_t T) :
   Result (hashmap_hash_map_t T)
   :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons k v tl =>
     do
       let ntable0 ← hashmap_hash_map_insert_no_resize_fwd_back T ntable k v
@@ -256,7 +258,7 @@ def hashmap_hash_map_insert_fwd_back
 /- [hashmap_main::hashmap::HashMap::{0}::contains_key_in_list] -/
 divergent def hashmap_hash_map_contains_key_in_list_loop_fwd
   (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result Bool :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey t tl =>
     if ckey = key
     then Result.ret true
@@ -282,7 +284,7 @@ def hashmap_hash_map_contains_key_fwd
 /- [hashmap_main::hashmap::HashMap::{0}::get_in_list] -/
 divergent def hashmap_hash_map_get_in_list_loop_fwd
   (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret cvalue
@@ -308,7 +310,7 @@ def hashmap_hash_map_get_fwd
 /- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list] -/
 divergent def hashmap_hash_map_get_mut_in_list_loop_fwd
   (T : Type) (ls : hashmap_list_t T) (key : Usize) : Result T :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret cvalue
@@ -325,7 +327,7 @@ divergent def hashmap_hash_map_get_mut_in_list_loop_back
   (T : Type) (ls : hashmap_list_t T) (key : Usize) (ret0 : T) :
   Result (hashmap_list_t T)
   :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey cvalue tl =>
     if ckey = key
     then Result.ret (hashmap_list_t.Cons ckey ret0 tl)
@@ -373,14 +375,14 @@ def hashmap_hash_map_get_mut_back
 /- [hashmap_main::hashmap::HashMap::{0}::remove_from_list] -/
 divergent def hashmap_hash_map_remove_from_list_loop_fwd
   (T : Type) (key : Usize) (ls : hashmap_list_t T) : Result (Option T) :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey t tl =>
     if ckey = key
     then
       let mv_ls :=
         mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
           hashmap_list_t.Nil
-      match h: mv_ls with
+      match mv_ls with
       | hashmap_list_t.Cons i cvalue tl0 => Result.ret (Option.some cvalue)
       | hashmap_list_t.Nil => Result.fail Error.panic
     else hashmap_hash_map_remove_from_list_loop_fwd T key tl
@@ -396,14 +398,14 @@ divergent def hashmap_hash_map_remove_from_list_loop_back
   (T : Type) (key : Usize) (ls : hashmap_list_t T) :
   Result (hashmap_list_t T)
   :=
-  match h: ls with
+  match ls with
   | hashmap_list_t.Cons ckey t tl =>
     if ckey = key
     then
       let mv_ls :=
         mem_replace_fwd (hashmap_list_t T) (hashmap_list_t.Cons ckey t tl)
           hashmap_list_t.Nil
-      match h: mv_ls with
+      match mv_ls with
       | hashmap_list_t.Cons i cvalue tl0 => Result.ret tl0
       | hashmap_list_t.Nil => Result.fail Error.panic
     else
@@ -429,7 +431,7 @@ def hashmap_hash_map_remove_fwd
     let l ←
       vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
     let x ← hashmap_hash_map_remove_from_list_fwd T key l
-    match h: x with
+    match x with
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
@@ -449,7 +451,7 @@ def hashmap_hash_map_remove_back
     let l ←
       vec_index_mut_fwd (hashmap_list_t T) self.hashmap_hash_map_slots hash_mod
     let x ← hashmap_hash_map_remove_from_list_fwd T key l
-    match h: x with
+    match x with
     | Option.none =>
       do
         let l0 ← hashmap_hash_map_remove_from_list_back T key l
@@ -505,7 +507,7 @@ def hashmap_test1_fwd : Result Unit :=
             let x ←
               hashmap_hash_map_remove_fwd U64 hm4
                 (Usize.ofInt 1024 (by intlit))
-            match h: x with
+            match x with
             | Option.none => Result.fail Error.panic
             | Option.some x0 =>
               if not (x0 = (U64.ofInt 56 (by intlit)))
@@ -555,3 +557,4 @@ def main_fwd : Result Unit :=
 /- Unit test for [hashmap_main::main] -/
 #assert (main_fwd == .ret ())
 
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean
index bef4f3fb..10e4d8bd 100644
--- a/tests/lean/HashmapMain/Opaque.lean
+++ b/tests/lean/HashmapMain/Opaque.lean
@@ -4,13 +4,16 @@ import Base
 import HashmapMain.Types
 open Primitives
 
+namespace HashmapMain
+
 structure OpaqueDefs where
   
   /- [hashmap_main::hashmap_utils::deserialize] -/
   hashmap_utils_deserialize_fwd
-    : State -> Result (State × (hashmap_hash_map_t U64))
+    : State → Result (State × (hashmap_hash_map_t U64))
   
   /- [hashmap_main::hashmap_utils::serialize] -/
   hashmap_utils_serialize_fwd
-    : hashmap_hash_map_t U64 -> State -> Result (State × Unit)
+    : hashmap_hash_map_t U64 → State → Result (State × Unit)
   
+end HashmapMain
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index 858e1c51..b91ff3a7 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -3,9 +3,11 @@
 import Base
 open Primitives
 
+namespace HashmapMain
+
 /- [hashmap_main::hashmap::List] -/
 inductive hashmap_list_t (T : Type) :=
-| Cons : Usize -> T -> hashmap_list_t T -> hashmap_list_t T
+| Cons : Usize → T → hashmap_list_t T → hashmap_list_t T
 | Nil : hashmap_list_t T
 
 /- [hashmap_main::hashmap::HashMap] -/
@@ -18,3 +20,4 @@ structure hashmap_hash_map_t (T : Type) where
 /- The state type used in the state-error monad -/
 axiom State : Type
 
+end HashmapMain
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 7d5f7595..9e084327 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -4,6 +4,8 @@ import Base
 import Loops.Types
 open Primitives
 
+namespace Loops
+
 /- [loops::sum] -/
 divergent def sum_loop_fwd (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -68,7 +70,7 @@ def clear_fwd_back (v : Vec U32) : Result (Vec U32) :=
 
 /- [loops::list_mem] -/
 divergent def list_mem_loop_fwd (x : U32) (ls : list_t U32) : Result Bool :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret true
@@ -82,7 +84,7 @@ def list_mem_fwd (x : U32) (ls : list_t U32) : Result Bool :=
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : U32) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -99,7 +101,7 @@ def list_nth_mut_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
 /- [loops::list_nth_mut_loop] -/
 divergent def list_nth_mut_loop_loop_back
   (T : Type) (ls : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -118,7 +120,7 @@ def list_nth_mut_loop_back
 /- [loops::list_nth_shared_loop] -/
 divergent def list_nth_shared_loop_loop_fwd
   (T : Type) (ls : list_t T) (i : U32) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -135,7 +137,7 @@ def list_nth_shared_loop_fwd (T : Type) (ls : list_t T) (i : U32) : Result T :=
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_fwd
   (x : Usize) (ls : list_t Usize) : Result Usize :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret y
@@ -152,7 +154,7 @@ def get_elem_mut_fwd (slots : Vec (list_t Usize)) (x : Usize) : Result Usize :=
 /- [loops::get_elem_mut] -/
 divergent def get_elem_mut_loop_back
   (x : Usize) (ls : list_t Usize) (ret0 : Usize) : Result (list_t Usize) :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret (list_t.Cons ret0 tl)
@@ -176,7 +178,7 @@ def get_elem_mut_back
 /- [loops::get_elem_shared] -/
 divergent def get_elem_shared_loop_fwd
   (x : Usize) (ls : list_t Usize) : Result Usize :=
-  match h: ls with
+  match ls with
   | list_t.Cons y tl =>
     if y = x
     then Result.ret y
@@ -206,7 +208,7 @@ def id_shared_fwd (T : Type) (ls : list_t T) : Result (list_t T) :=
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_fwd
   (T : Type) (i : U32) (ls : list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -226,7 +228,7 @@ def list_nth_mut_loop_with_id_fwd
 /- [loops::list_nth_mut_loop_with_id] -/
 divergent def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : U32) (ls : list_t T) (ret0 : T) : Result (list_t T) :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -248,7 +250,7 @@ def list_nth_mut_loop_with_id_back
 /- [loops::list_nth_shared_loop_with_id] -/
 divergent def list_nth_shared_loop_with_id_loop_fwd
   (T : Type) (i : U32) (ls : list_t T) : Result T :=
-  match h: ls with
+  match ls with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -268,9 +270,9 @@ def list_nth_shared_loop_with_id_fwd
 /- [loops::list_nth_mut_loop_pair] -/
 divergent def list_nth_mut_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -291,9 +293,9 @@ divergent def list_nth_mut_loop_pair_loop_back'a
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -317,9 +319,9 @@ divergent def list_nth_mut_loop_pair_loop_back'b
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -341,9 +343,9 @@ def list_nth_mut_loop_pair_back'b
 /- [loops::list_nth_shared_loop_pair] -/
 divergent def list_nth_shared_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -362,9 +364,9 @@ def list_nth_shared_loop_pair_fwd
 /- [loops::list_nth_mut_loop_pair_merge] -/
 divergent def list_nth_mut_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -385,9 +387,9 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : (T × T)) :
   Result ((list_t T) × (list_t T))
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then
@@ -412,9 +414,9 @@ def list_nth_mut_loop_pair_merge_back
 /- [loops::list_nth_shared_loop_pair_merge] -/
 divergent def list_nth_shared_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -433,9 +435,9 @@ def list_nth_shared_loop_pair_merge_fwd
 /- [loops::list_nth_mut_shared_loop_pair] -/
 divergent def list_nth_mut_shared_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -456,9 +458,9 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -481,9 +483,9 @@ def list_nth_mut_shared_loop_pair_back
 /- [loops::list_nth_mut_shared_loop_pair_merge] -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -504,9 +506,9 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl0)
@@ -529,9 +531,9 @@ def list_nth_mut_shared_loop_pair_merge_back
 /- [loops::list_nth_shared_mut_loop_pair] -/
 divergent def list_nth_shared_mut_loop_pair_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -552,9 +554,9 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -577,9 +579,9 @@ def list_nth_shared_mut_loop_pair_back
 /- [loops::list_nth_shared_mut_loop_pair_merge] -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop_fwd
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) : Result (T × T) :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (x0, x1)
@@ -600,9 +602,9 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
   (T : Type) (ls0 : list_t T) (ls1 : list_t T) (i : U32) (ret0 : T) :
   Result (list_t T)
   :=
-  match h: ls0 with
+  match ls0 with
   | list_t.Cons x0 tl0 =>
-    match h: ls1 with
+    match ls1 with
     | list_t.Cons x1 tl1 =>
       if i = (U32.ofInt 0 (by intlit))
       then Result.ret (list_t.Cons ret0 tl1)
@@ -622,3 +624,4 @@ def list_nth_shared_mut_loop_pair_merge_back
   :=
   list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
 
+end Loops
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index e14f9766..ca0403e9 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -3,8 +3,11 @@
 import Base
 open Primitives
 
+namespace Loops
+
 /- [loops::List] -/
 inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
 | Nil : list_t T
 
+end Loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 67ef4b20..769bb311 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -3,6 +3,8 @@
 import Base
 open Primitives
 
+namespace NoNestedBorrows
+
 /- [no_nested_borrows::Pair] -/
 structure pair_t (T1 T2 : Type) where
   pair_x : T1
@@ -10,12 +12,12 @@ structure pair_t (T1 T2 : Type) where
 
 /- [no_nested_borrows::List] -/
 inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
 | Nil : list_t T
 
 /- [no_nested_borrows::One] -/
 inductive one_t (T1 : Type) :=
-| One : T1 -> one_t T1
+| One : T1 → one_t T1
 
 /- [no_nested_borrows::EmptyEnum] -/
 inductive empty_enum_t :=
@@ -31,8 +33,8 @@ structure empty_struct_t where
 
 /- [no_nested_borrows::Sum] -/
 inductive sum_t (T1 T2 : Type) :=
-| Left : T1 -> sum_t T1 T2
-| Right : T2 -> sum_t T1 T2
+| Left : T1 → sum_t T1 T2
+| Right : T2 → sum_t T1 T2
 
 /- [no_nested_borrows::neg_test] -/
 def neg_test_fwd (x : I32) : Result I32 :=
@@ -175,7 +177,7 @@ def test_copy_int_fwd : Result Unit :=
 
 /- [no_nested_borrows::is_cons] -/
 def is_cons_fwd (T : Type) (l : list_t T) : Result Bool :=
-  match h: l with
+  match l with
   | list_t.Cons t l0 => Result.ret true
   | list_t.Nil => Result.ret false
 
@@ -193,7 +195,7 @@ def test_is_cons_fwd : Result Unit :=
 
 /- [no_nested_borrows::split_list] -/
 def split_list_fwd (T : Type) (l : list_t T) : Result (T × (list_t T)) :=
-  match h: l with
+  match l with
   | list_t.Cons hd tl => Result.ret (hd, tl)
   | list_t.Nil => Result.fail Error.panic
 
@@ -254,19 +256,19 @@ mutual
 
 /- [no_nested_borrows::NodeElem] -/
 inductive node_elem_t (T : Type) :=
-| Cons : tree_t T -> node_elem_t T -> node_elem_t T
+| Cons : tree_t T → node_elem_t T → node_elem_t T
 | Nil : node_elem_t T
 
 /- [no_nested_borrows::Tree] -/
 inductive tree_t (T : Type) :=
-| Leaf : T -> tree_t T
-| Node : T -> node_elem_t T -> tree_t T -> tree_t T
+| Leaf : T → tree_t T
+| Node : T → node_elem_t T → tree_t T → tree_t T
 
 end
 
 /- [no_nested_borrows::list_length] -/
 divergent def list_length_fwd (T : Type) (l : list_t T) : Result U32 :=
-  match h: l with
+  match l with
   | list_t.Cons t l1 =>
     do
       let i ← list_length_fwd T l1
@@ -276,7 +278,7 @@ divergent def list_length_fwd (T : Type) (l : list_t T) : Result U32 :=
 /- [no_nested_borrows::list_nth_shared] -/
 divergent def list_nth_shared_fwd
   (T : Type) (l : list_t T) (i : U32) : Result T :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -289,7 +291,7 @@ divergent def list_nth_shared_fwd
 /- [no_nested_borrows::list_nth_mut] -/
 divergent def list_nth_mut_fwd
   (T : Type) (l : list_t T) (i : U32) : Result T :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -301,7 +303,7 @@ divergent def list_nth_mut_fwd
 /- [no_nested_borrows::list_nth_mut] -/
 divergent def list_nth_mut_back
   (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -315,7 +317,7 @@ divergent def list_nth_mut_back
 /- [no_nested_borrows::list_rev_aux] -/
 divergent def list_rev_aux_fwd
   (T : Type) (li : list_t T) (lo : list_t T) : Result (list_t T) :=
-  match h: li with
+  match li with
   | list_t.Cons hd tl => list_rev_aux_fwd T tl (list_t.Cons hd lo)
   | list_t.Nil => Result.ret lo
 
@@ -531,7 +533,7 @@ def test_shared_borrow_bool2_fwd : Result U32 :=
 
 /- [no_nested_borrows::test_shared_borrow_enum1] -/
 def test_shared_borrow_enum1_fwd (l : list_t U32) : Result U32 :=
-  match h: l with
+  match l with
   | list_t.Cons i l0 => Result.ret (U32.ofInt 1 (by intlit))
   | list_t.Nil => Result.ret (U32.ofInt 0 (by intlit))
 
@@ -539,3 +541,4 @@ def test_shared_borrow_enum1_fwd (l : list_t U32) : Result U32 :=
 def test_shared_borrow_enum2_fwd : Result U32 :=
   Result.ret (U32.ofInt 0 (by intlit))
 
+end NoNestedBorrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 9019b694..edcb5c1b 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -3,6 +3,8 @@
 import Base
 open Primitives
 
+namespace Paper
+
 /- [paper::ref_incr] -/
 def ref_incr_fwd_back (x : I32) : Result I32 :=
   x + (I32.ofInt 1 (by intlit))
@@ -56,13 +58,13 @@ def test_choose_fwd : Result Unit :=
 
 /- [paper::List] -/
 inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
 | Nil : list_t T
 
 /- [paper::list_nth_mut] -/
 divergent def list_nth_mut_fwd
   (T : Type) (l : list_t T) (i : U32) : Result T :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret x
@@ -74,7 +76,7 @@ divergent def list_nth_mut_fwd
 /- [paper::list_nth_mut] -/
 divergent def list_nth_mut_back
   (T : Type) (l : list_t T) (i : U32) (ret0 : T) : Result (list_t T) :=
-  match h: l with
+  match l with
   | list_t.Cons x tl =>
     if i = (U32.ofInt 0 (by intlit))
     then Result.ret (list_t.Cons ret0 tl)
@@ -87,7 +89,7 @@ divergent def list_nth_mut_back
 
 /- [paper::sum] -/
 divergent def sum_fwd (l : list_t I32) : Result I32 :=
-  match h: l with
+  match l with
   | list_t.Cons x tl => do
                           let i ← sum_fwd tl
                           x + i
@@ -123,3 +125,4 @@ def call_choose_fwd (p : (U32 × U32)) : Result U32 :=
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
 
+end Paper
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 671f54ea..0f2a05e3 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -3,15 +3,17 @@
 import Base
 open Primitives
 
+namespace PoloniusList
+
 /- [polonius_list::List] -/
 inductive list_t (T : Type) :=
-| Cons : T -> list_t T -> list_t T
+| Cons : T → list_t T → list_t T
 | Nil : list_t T
 
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_fwd
   (ls : list_t U32) (x : U32) : Result (list_t U32) :=
-  match h: ls with
+  match ls with
   | list_t.Cons hd tl =>
     if hd = x
     then Result.ret (list_t.Cons hd tl)
@@ -21,7 +23,7 @@ divergent def get_list_at_x_fwd
 /- [polonius_list::get_list_at_x] -/
 divergent def get_list_at_x_back
   (ls : list_t U32) (x : U32) (ret0 : list_t U32) : Result (list_t U32) :=
-  match h: ls with
+  match ls with
   | list_t.Cons hd tl =>
     if hd = x
     then Result.ret ret0
@@ -31,3 +33,4 @@ divergent def get_list_at_x_back
         Result.ret (list_t.Cons hd tl0)
   | list_t.Nil => Result.ret ret0
 
+end PoloniusList
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 1397c6f0..ccd6d61a 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -11,7 +11,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "cb02d09e1d5611d22efc2b406e7893f246b2f51e",
+    "rev": "409bee4eabf8072c4569950c3c2f310afd203abf",
     "name": "mathlib",
     "inputRev?": null}},
   {"git":
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index da4293dd..217e533f 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -11,4 +11,12 @@ package «tests» {}
 @[default_target]
 lean_lib «Tests» {}
 
+lean_lib betreeMain
+lean_lib constants
+lean_lib external
 lean_lib hashmap
+lean_lib hashmapMain
+lean_lib loops
+lean_lib noNestedBorrows
+lean_lib paper
+lean_lib poloniusList