Merge branch 'main' into son/loops2

34 files changed, 610 insertions, 1021 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 5ffcce51..c2c3ac90 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -6,24 +6,24 @@ open Primitives
 namespace arrays
 
 /- [arrays::AB]
-   Source: 'tests/src/arrays.rs', lines 3:0-3:11 -/
+   Source: 'tests/src/arrays.rs', lines 6:0-6:11 -/
 inductive AB :=
 | A : AB
 | B : AB
 
 /- [arrays::incr]:
-   Source: 'tests/src/arrays.rs', lines 8:0-8:24 -/
+   Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
 /- [arrays::array_to_shared_slice_]:
-   Source: 'tests/src/arrays.rs', lines 16:0-16:53 -/
+   Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/
 def array_to_shared_slice_
   (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
   Array.to_slice T 32#usize s
 
 /- [arrays::array_to_mut_slice_]:
-   Source: 'tests/src/arrays.rs', lines 21:0-21:58 -/
+   Source: 'tests/src/arrays.rs', lines 24:0-24:58 -/
 def array_to_mut_slice_
   (T : Type) (s : Array T 32#usize) :
   Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
@@ -31,42 +31,42 @@ def array_to_mut_slice_
   Array.to_slice_mut T 32#usize s
 
 /- [arrays::array_len]:
-   Source: 'tests/src/arrays.rs', lines 25:0-25:40 -/
+   Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
   Result.ok (Slice.len T s1)
 
 /- [arrays::shared_array_len]:
-   Source: 'tests/src/arrays.rs', lines 29:0-29:48 -/
+   Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
   Result.ok (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
-   Source: 'tests/src/arrays.rs', lines 33:0-33:44 -/
+   Source: 'tests/src/arrays.rs', lines 36:0-36:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
   Result.ok (Slice.len T s)
 
 /- [arrays::index_array_shared]:
-   Source: 'tests/src/arrays.rs', lines 37:0-37:57 -/
+   Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/
 def index_array_shared
   (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
   Array.index_usize T 32#usize s i
 
 /- [arrays::index_array_u32]:
-   Source: 'tests/src/arrays.rs', lines 44:0-44:53 -/
+   Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/
 def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 :=
   Array.index_usize U32 32#usize s i
 
 /- [arrays::index_array_copy]:
-   Source: 'tests/src/arrays.rs', lines 48:0-48:45 -/
+   Source: 'tests/src/arrays.rs', lines 51:0-51:45 -/
 def index_array_copy (x : Array U32 32#usize) : Result U32 :=
   Array.index_usize U32 32#usize x 0#usize
 
 /- [arrays::index_mut_array]:
-   Source: 'tests/src/arrays.rs', lines 52:0-52:62 -/
+   Source: 'tests/src/arrays.rs', lines 55:0-55:62 -/
 def index_mut_array
   (T : Type) (s : Array T 32#usize) (i : Usize) :
   Result (T × (T → Result (Array T 32#usize)))
@@ -74,12 +74,12 @@ def index_mut_array
   Array.index_mut_usize T 32#usize s i
 
 /- [arrays::index_slice]:
-   Source: 'tests/src/arrays.rs', lines 56:0-56:46 -/
+   Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/
 def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
   Slice.index_usize T s i
 
 /- [arrays::index_mut_slice]:
-   Source: 'tests/src/arrays.rs', lines 60:0-60:58 -/
+   Source: 'tests/src/arrays.rs', lines 63:0-63:58 -/
 def index_mut_slice
   (T : Type) (s : Slice T) (i : Usize) :
   Result (T × (T → Result (Slice T)))
@@ -87,7 +87,7 @@ def index_mut_slice
   Slice.index_mut_usize T s i
 
 /- [arrays::slice_subslice_shared_]:
-   Source: 'tests/src/arrays.rs', lines 64:0-64:70 -/
+   Source: 'tests/src/arrays.rs', lines 67:0-67:70 -/
 def slice_subslice_shared_
   (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) :=
   core.slice.index.Slice.index U32 (core.ops.range.Range Usize)
@@ -95,7 +95,7 @@ def slice_subslice_shared_
     { start := y, end_ := z }
 
 /- [arrays::slice_subslice_mut_]:
-   Source: 'tests/src/arrays.rs', lines 68:0-68:75 -/
+   Source: 'tests/src/arrays.rs', lines 71:0-71:75 -/
 def slice_subslice_mut_
   (x : Slice U32) (y : Usize) (z : Usize) :
   Result ((Slice U32) × (Slice U32 → Result (Slice U32)))
@@ -108,12 +108,12 @@ def slice_subslice_mut_
   Result.ok (s, index_mut_back)
 
 /- [arrays::array_to_slice_shared_]:
-   Source: 'tests/src/arrays.rs', lines 72:0-72:54 -/
+   Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/
 def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) :=
   Array.to_slice U32 32#usize x
 
 /- [arrays::array_to_slice_mut_]:
-   Source: 'tests/src/arrays.rs', lines 76:0-76:59 -/
+   Source: 'tests/src/arrays.rs', lines 79:0-79:59 -/
 def array_to_slice_mut_
   (x : Array U32 32#usize) :
   Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
@@ -121,7 +121,7 @@ def array_to_slice_mut_
   Array.to_slice_mut U32 32#usize x
 
 /- [arrays::array_subslice_shared_]:
-   Source: 'tests/src/arrays.rs', lines 80:0-80:74 -/
+   Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/
 def array_subslice_shared_
   (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
   core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
@@ -130,7 +130,7 @@ def array_subslice_shared_
     { start := y, end_ := z }
 
 /- [arrays::array_subslice_mut_]:
-   Source: 'tests/src/arrays.rs', lines 84:0-84:79 -/
+   Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/
 def array_subslice_mut_
   (x : Array U32 32#usize) (y : Usize) (z : Usize) :
   Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
@@ -144,17 +144,17 @@ def array_subslice_mut_
   Result.ok (s, index_mut_back)
 
 /- [arrays::index_slice_0]:
-   Source: 'tests/src/arrays.rs', lines 88:0-88:38 -/
+   Source: 'tests/src/arrays.rs', lines 91:0-91:38 -/
 def index_slice_0 (T : Type) (s : Slice T) : Result T :=
   Slice.index_usize T s 0#usize
 
 /- [arrays::index_array_0]:
-   Source: 'tests/src/arrays.rs', lines 92:0-92:42 -/
+   Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/
 def index_array_0 (T : Type) (s : Array T 32#usize) : Result T :=
   Array.index_usize T 32#usize s 0#usize
 
 /- [arrays::index_index_array]:
-   Source: 'tests/src/arrays.rs', lines 103:0-103:71 -/
+   Source: 'tests/src/arrays.rs', lines 106:0-106:71 -/
 def index_index_array
   (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
   Result U32
@@ -164,7 +164,7 @@ def index_index_array
   Array.index_usize U32 32#usize a j
 
 /- [arrays::update_update_array]:
-   Source: 'tests/src/arrays.rs', lines 114:0-114:70 -/
+   Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/
 def update_update_array
   (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
   Result Unit
@@ -178,37 +178,37 @@ def update_update_array
   Result.ok ()
 
 /- [arrays::array_local_deep_copy]:
-   Source: 'tests/src/arrays.rs', lines 118:0-118:43 -/
+   Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/
 def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_array]:
-   Source: 'tests/src/arrays.rs', lines 122:0-122:30 -/
+   Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/
 def take_array (a : Array U32 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_array_borrow]:
-   Source: 'tests/src/arrays.rs', lines 123:0-123:38 -/
+   Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/
 def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_slice]:
-   Source: 'tests/src/arrays.rs', lines 124:0-124:28 -/
+   Source: 'tests/src/arrays.rs', lines 127:0-127:28 -/
 def take_slice (s : Slice U32) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_mut_slice]:
-   Source: 'tests/src/arrays.rs', lines 125:0-125:36 -/
+   Source: 'tests/src/arrays.rs', lines 128:0-128:36 -/
 def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
   Result.ok s
 
 /- [arrays::const_array]:
-   Source: 'tests/src/arrays.rs', lines 127:0-127:32 -/
+   Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/
 def const_array : Result (Array U32 2#usize) :=
   Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
 
 /- [arrays::const_slice]:
-   Source: 'tests/src/arrays.rs', lines 131:0-131:20 -/
+   Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/
 def const_slice : Result Unit :=
   do
   let _ ←
@@ -216,7 +216,7 @@ def const_slice : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_all]:
-   Source: 'tests/src/arrays.rs', lines 141:0-141:17 -/
+   Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/
 def take_all : Result Unit :=
   do
   let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -232,29 +232,29 @@ def take_all : Result Unit :=
   Result.ok ()
 
 /- [arrays::index_array]:
-   Source: 'tests/src/arrays.rs', lines 155:0-155:38 -/
+   Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/
 def index_array (x : Array U32 2#usize) : Result U32 :=
   Array.index_usize U32 2#usize x 0#usize
 
 /- [arrays::index_array_borrow]:
-   Source: 'tests/src/arrays.rs', lines 158:0-158:46 -/
+   Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/
 def index_array_borrow (x : Array U32 2#usize) : Result U32 :=
   Array.index_usize U32 2#usize x 0#usize
 
 /- [arrays::index_slice_u32_0]:
-   Source: 'tests/src/arrays.rs', lines 162:0-162:42 -/
+   Source: 'tests/src/arrays.rs', lines 165:0-165:42 -/
 def index_slice_u32_0 (x : Slice U32) : Result U32 :=
   Slice.index_usize U32 x 0#usize
 
 /- [arrays::index_mut_slice_u32_0]:
-   Source: 'tests/src/arrays.rs', lines 166:0-166:50 -/
+   Source: 'tests/src/arrays.rs', lines 169:0-169:50 -/
 def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) :=
   do
   let i ← Slice.index_usize U32 x 0#usize
   Result.ok (i, x)
 
 /- [arrays::index_all]:
-   Source: 'tests/src/arrays.rs', lines 170:0-170:25 -/
+   Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/
 def index_all : Result U32 :=
   do
   let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -274,7 +274,7 @@ def index_all : Result U32 :=
   Result.ok i8
 
 /- [arrays::update_array]:
-   Source: 'tests/src/arrays.rs', lines 184:0-184:36 -/
+   Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
 def update_array (x : Array U32 2#usize) : Result Unit :=
   do
   let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
@@ -282,7 +282,7 @@ def update_array (x : Array U32 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::update_array_mut_borrow]:
-   Source: 'tests/src/arrays.rs', lines 187:0-187:48 -/
+   Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/
 def update_array_mut_borrow
   (x : Array U32 2#usize) : Result (Array U32 2#usize) :=
   do
@@ -290,14 +290,14 @@ def update_array_mut_borrow
   index_mut_back 1#u32
 
 /- [arrays::update_mut_slice]:
-   Source: 'tests/src/arrays.rs', lines 190:0-190:38 -/
+   Source: 'tests/src/arrays.rs', lines 193:0-193:38 -/
 def update_mut_slice (x : Slice U32) : Result (Slice U32) :=
   do
   let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize
   index_mut_back 1#u32
 
 /- [arrays::update_all]:
-   Source: 'tests/src/arrays.rs', lines 194:0-194:19 -/
+   Source: 'tests/src/arrays.rs', lines 197:0-197:19 -/
 def update_all : Result Unit :=
   do
   let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -309,7 +309,7 @@ def update_all : Result Unit :=
   Result.ok ()
 
 /- [arrays::range_all]:
-   Source: 'tests/src/arrays.rs', lines 205:0-205:18 -/
+   Source: 'tests/src/arrays.rs', lines 208:0-208:18 -/
 def range_all : Result Unit :=
   do
   let (s, index_mut_back) ←
@@ -323,12 +323,12 @@ def range_all : Result Unit :=
   Result.ok ()
 
 /- [arrays::deref_array_borrow]:
-   Source: 'tests/src/arrays.rs', lines 214:0-214:46 -/
+   Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/
 def deref_array_borrow (x : Array U32 2#usize) : Result U32 :=
   Array.index_usize U32 2#usize x 0#usize
 
 /- [arrays::deref_array_mut_borrow]:
-   Source: 'tests/src/arrays.rs', lines 219:0-219:54 -/
+   Source: 'tests/src/arrays.rs', lines 222:0-222:54 -/
 def deref_array_mut_borrow
   (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
   do
@@ -336,17 +336,17 @@ def deref_array_mut_borrow
   Result.ok (i, x)
 
 /- [arrays::take_array_t]:
-   Source: 'tests/src/arrays.rs', lines 227:0-227:31 -/
+   Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/
 def take_array_t (a : Array AB 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::non_copyable_array]:
-   Source: 'tests/src/arrays.rs', lines 229:0-229:27 -/
+   Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/
 def non_copyable_array : Result Unit :=
   take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 242:0-250:1 -/
+   Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
 divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len U32 s
   if i < i1
@@ -359,12 +359,12 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   else Result.ok sum1
 
 /- [arrays::sum]:
-   Source: 'tests/src/arrays.rs', lines 242:0-242:28 -/
+   Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/
 def sum (s : Slice U32) : Result U32 :=
   sum_loop s 0#u32 0#usize
 
 /- [arrays::sum2]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 252:0-261:1 -/
+   Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
 divergent def sum2_loop
   (s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
   let i1 := Slice.len U32 s
@@ -380,7 +380,7 @@ divergent def sum2_loop
   else Result.ok sum1
 
 /- [arrays::sum2]:
-   Source: 'tests/src/arrays.rs', lines 252:0-252:41 -/
+   Source: 'tests/src/arrays.rs', lines 255:0-255:41 -/
 def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
   let i := Slice.len U32 s
   let i1 := Slice.len U32 s2
@@ -389,7 +389,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
   else sum2_loop s s2 0#u32 0#usize
 
 /- [arrays::f0]:
-   Source: 'tests/src/arrays.rs', lines 263:0-263:11 -/
+   Source: 'tests/src/arrays.rs', lines 266:0-266:11 -/
 def f0 : Result Unit :=
   do
   let (s, to_slice_mut_back) ←
@@ -400,7 +400,7 @@ def f0 : Result Unit :=
   Result.ok ()
 
 /- [arrays::f1]:
-   Source: 'tests/src/arrays.rs', lines 268:0-268:11 -/
+   Source: 'tests/src/arrays.rs', lines 271:0-271:11 -/
 def f1 : Result Unit :=
   do
   let (_, index_mut_back) ←
@@ -410,12 +410,12 @@ def f1 : Result Unit :=
   Result.ok ()
 
 /- [arrays::f2]:
-   Source: 'tests/src/arrays.rs', lines 273:0-273:17 -/
+   Source: 'tests/src/arrays.rs', lines 276:0-276:17 -/
 def f2 (i : U32) : Result Unit :=
   Result.ok ()
 
 /- [arrays::f4]:
-   Source: 'tests/src/arrays.rs', lines 282:0-282:54 -/
+   Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/
 def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
   core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
     (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize)
@@ -423,7 +423,7 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
     { start := y, end_ := z }
 
 /- [arrays::f3]:
-   Source: 'tests/src/arrays.rs', lines 275:0-275:18 -/
+   Source: 'tests/src/arrays.rs', lines 278:0-278:18 -/
 def f3 : Result U32 :=
   do
   let i ←
@@ -437,17 +437,17 @@ def f3 : Result U32 :=
   sum2 s s1
 
 /- [arrays::SZ]
-   Source: 'tests/src/arrays.rs', lines 286:0-286:19 -/
+   Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/
 def SZ_body : Result Usize := Result.ok 32#usize
 def SZ : Usize := eval_global SZ_body
 
 /- [arrays::f5]:
-   Source: 'tests/src/arrays.rs', lines 289:0-289:31 -/
+   Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/
 def f5 (x : Array U32 32#usize) : Result U32 :=
   Array.index_usize U32 32#usize x 0#usize
 
 /- [arrays::ite]:
-   Source: 'tests/src/arrays.rs', lines 294:0-294:12 -/
+   Source: 'tests/src/arrays.rs', lines 297:0-297:12 -/
 def ite : Result Unit :=
   do
   let (s, to_slice_mut_back) ←
@@ -461,7 +461,7 @@ def ite : Result Unit :=
   Result.ok ()
 
 /- [arrays::zero_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 303:0-310:1 -/
+   Source: 'tests/src/arrays.rs', lines 306:0-313:1 -/
 divergent def zero_slice_loop
   (a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
   if i < len
@@ -474,13 +474,13 @@ divergent def zero_slice_loop
   else Result.ok a
 
 /- [arrays::zero_slice]:
-   Source: 'tests/src/arrays.rs', lines 303:0-303:31 -/
+   Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/
 def zero_slice (a : Slice U8) : Result (Slice U8) :=
   let len := Slice.len U8 a
   zero_slice_loop a 0#usize len
 
 /- [arrays::iter_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 312:0-318:1 -/
+   Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/
 divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   if i < len
   then do
@@ -489,7 +489,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   else Result.ok ()
 
 /- [arrays::iter_mut_slice]:
-   Source: 'tests/src/arrays.rs', lines 312:0-312:35 -/
+   Source: 'tests/src/arrays.rs', lines 315:0-315:35 -/
 def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   do
   let len := Slice.len U8 a
@@ -497,7 +497,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
-   Source: 'tests/src/arrays.rs', lines 320:0-328:1 -/
+   Source: 'tests/src/arrays.rs', lines 323:0-331:1 -/
 divergent def sum_mut_slice_loop
   (a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
   let i1 := Slice.len U32 a
@@ -511,7 +511,7 @@ divergent def sum_mut_slice_loop
   else Result.ok s
 
 /- [arrays::sum_mut_slice]:
-   Source: 'tests/src/arrays.rs', lines 320:0-320:42 -/
+   Source: 'tests/src/arrays.rs', lines 323:0-323:42 -/
 def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
   do
   let i ← sum_mut_slice_loop a 0#usize 0#u32
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/Betree/Funs.lean
index 7cc52159..8612ccbc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -1,13 +1,13 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: function definitions
+-- [betree]: function definitions
 import Base
-import BetreeMain.Types
-import BetreeMain.FunsExternal
+import Betree.Types
+import Betree.FunsExternal
 open Primitives
 
-namespace betree_main
+namespace betree
 
-/- [betree_main::betree::load_internal_node]:
+/- [betree::betree::load_internal_node]:
    Source: 'src/betree.rs', lines 36:0-36:52 -/
 def betree.load_internal_node
   (id : U64) (st : State) :
@@ -15,7 +15,7 @@ def betree.load_internal_node
   :=
   betree_utils.load_internal_node id st
 
-/- [betree_main::betree::store_internal_node]:
+/- [betree::betree::store_internal_node]:
    Source: 'src/betree.rs', lines 41:0-41:60 -/
 def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
@@ -23,13 +23,13 @@ def betree.store_internal_node
   :=
   betree_utils.store_internal_node id content st
 
-/- [betree_main::betree::load_leaf_node]:
+/- [betree::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
 def betree.load_leaf_node
   (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) :=
   betree_utils.load_leaf_node id st
 
-/- [betree_main::betree::store_leaf_node]:
+/- [betree::betree::store_leaf_node]:
    Source: 'src/betree.rs', lines 51:0-51:52 -/
 def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
@@ -37,19 +37,19 @@ def betree.store_leaf_node
   :=
   betree_utils.store_leaf_node id content st
 
-/- [betree_main::betree::fresh_node_id]:
+/- [betree::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
 def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
   let counter1 ← counter + 1#u64
   Result.ok (counter, counter1)
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
+/- [betree::betree::{betree::betree::NodeIdCounter}::new]:
    Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ok { next_node_id := 0#u64 }
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
+/- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]:
    Source: 'src/betree.rs', lines 210:4-210:36 -/
 def betree.NodeIdCounter.fresh_id
   (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
@@ -57,7 +57,7 @@ def betree.NodeIdCounter.fresh_id
   let i ← self.next_node_id + 1#u64
   Result.ok (self.next_node_id, { next_node_id := i })
 
-/- [betree_main::betree::upsert_update]:
+/- [betree::betree::upsert_update]:
    Source: 'src/betree.rs', lines 234:0-234:70 -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -79,7 +79,7 @@ def betree.upsert_update
       then prev1 - v
       else Result.ok 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
+/- [betree::betree::{betree::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
@@ -88,7 +88,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
                              1#u64 + i
   | betree.List.Nil => Result.ok 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
+/- [betree::betree::{betree::betree::List<T>#1}::split_at]:
    Source: 'src/betree.rs', lines 284:4-284:51 -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
@@ -106,14 +106,14 @@ divergent def betree.List.split_at
       Result.ok (betree.List.Cons hd ls0, ls1)
     | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
+/- [betree::betree::{betree::betree::List<T>#1}::push_front]:
    Source: 'src/betree.rs', lines 299:4-299:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
   Result.ok (betree.List.Cons x tl)
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
+/- [betree::betree::{betree::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 306:4-306:32 -/
 def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
@@ -122,14 +122,14 @@ def betree.List.pop_front
   | betree.List.Cons x tl => Result.ok (x, tl)
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
+/- [betree::betree::{betree::betree::List<T>#1}::hd]:
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
   | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]:
    Source: 'src/betree.rs', lines 327:4-327:44 -/
 def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
@@ -138,7 +138,7 @@ def betree.ListPairU64T.head_has_key
                              Result.ok (i = key)
   | betree.List.Nil => Result.ok false
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
+/- [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
 divergent def betree.ListPairU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
@@ -156,7 +156,7 @@ divergent def betree.ListPairU64T.partition_at_pivot
       Result.ok (betree.List.Cons (i, t) ls0, ls1)
   | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
+/- [betree::betree::{betree::betree::Leaf#3}::split]:
    Source: 'src/betree.rs', lines 359:4-364:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
@@ -176,7 +176,7 @@ def betree.Leaf.split
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
   Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -200,7 +200,7 @@ divergent def betree.Node.lookup_first_message_for_key
       Result.ok (l, back)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 636:4-636:80 -/
 divergent def betree.Node.lookup_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
@@ -215,7 +215,7 @@ divergent def betree.Node.lookup_in_bindings
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ok none
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
+/- [betree::betree::{betree::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
@@ -244,24 +244,23 @@ divergent def betree.Node.apply_upserts
         betree.Message.Insert v)
     Result.ok (v, msgs1)
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
+/- [betree::betree::{betree::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
   :=
-  let ⟨ i, i1, n, n1 ⟩ := self
-  if key < i1
+  if key < self.pivot
   then
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
+    let (st1, (o, n)) ← betree.Node.lookup self.left key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right))
   else
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n1 key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
+    let (st1, (o, n)) ← betree.Node.lookup self.right key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
+/- [betree::betree::{betree::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
@@ -270,8 +269,7 @@ divergent def betree.Node.lookup
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, msgs) ← betree.load_internal_node i st
+    let (st1, msgs) ← betree.load_internal_node node.id st
     let (pending, lookup_first_message_for_key_back) ←
       betree.Node.lookup_first_message_for_key key msgs
     match pending with
@@ -281,8 +279,7 @@ divergent def betree.Node.lookup
       then
         do
         let (st2, (o, node1)) ←
-          betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-            st1
+          betree.Internal.lookup_in_children node key st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
         Result.ok (st2, (o, betree.Node.Internal node1))
@@ -293,33 +290,26 @@ divergent def betree.Node.lookup
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Insert v) l)
-          Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
-            i1 n n1)))
+          Result.ok (st1, (some v, betree.Node.Internal node))
         | betree.Message.Delete =>
           do
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Delete) l)
-          Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
-            n n1)))
+          Result.ok (st1, (none, betree.Node.Internal node))
         | betree.Message.Upsert ufs =>
           do
           let (st2, (v, node1)) ←
-            betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
-              key st1
+            betree.Internal.lookup_in_children node key st1
           let (v1, pending1) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
               betree.Message.Upsert ufs) l) v key
-          let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
-          let (st3, _) ← betree.store_internal_node i2 msgs1 st2
-          Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2
-            i3 n2 n3)))
+          let (st3, _) ← betree.store_internal_node node1.id msgs1 st2
+          Result.ok (st3, (some v1, betree.Node.Internal node1))
     | betree.List.Nil =>
       do
-      let (st2, (o, node1)) ←
-        betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-          st1
+      let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
       Result.ok (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
@@ -330,7 +320,7 @@ divergent def betree.Node.lookup
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
+/- [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]:
    Source: 'src/betree.rs', lines 674:4-674:77 -/
 divergent def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -349,7 +339,7 @@ divergent def betree.Node.filter_messages_for_key
     else Result.ok (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ok betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -373,7 +363,7 @@ divergent def betree.Node.lookup_first_message_after_key
     else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
+/- [betree::betree::{betree::betree::Node#5}::apply_to_internal]:
    Source: 'src/betree.rs', lines 521:4-521:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
@@ -437,7 +427,7 @@ def betree.Node.apply_to_internal
       betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
     lookup_first_message_for_key_back msgs2
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 502:4-505:5 -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
@@ -452,7 +442,7 @@ divergent def betree.Node.apply_messages_to_internal
     betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
   | betree.List.Nil => Result.ok msgs
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
+/- [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 653:4-656:32 -/
 divergent def betree.Node.lookup_mut_in_bindings
   (key : U64) (bindings : betree.List (U64 × U64)) :
@@ -476,7 +466,7 @@ divergent def betree.Node.lookup_mut_in_bindings
       Result.ok (l, back)
   | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
+/- [betree::betree::{betree::betree::Node#5}::apply_to_leaf]:
    Source: 'src/betree.rs', lines 460:4-460:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
@@ -516,7 +506,7 @@ def betree.Node.apply_to_leaf
       let bindings2 ← betree.List.push_front (U64 × U64) bindings1 (key, v)
       lookup_mut_in_bindings_back bindings2
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 444:4-447:5 -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
@@ -531,7 +521,7 @@ divergent def betree.Node.apply_messages_to_leaf
     betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
   | betree.List.Nil => Result.ok bindings
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
+/- [betree::betree::{betree::betree::Internal#4}::flush]:
    Source: 'src/betree.rs', lines 410:4-415:26 -/
 mutual divergent def betree.Internal.flush
   (self : betree.Internal) (params : betree.Params)
@@ -541,36 +531,38 @@ mutual divergent def betree.Internal.flush
     × betree.NodeIdCounter)))
   :=
   do
-  let ⟨ i, i1, n, n1 ⟩ := self
-  let p ← betree.ListPairU64T.partition_at_pivot betree.Message content i1
+  let p ←
+    betree.ListPairU64T.partition_at_pivot betree.Message content self.pivot
   let (msgs_left, msgs_right) := p
   let len_left ← betree.List.len (U64 × betree.Message) msgs_left
   if len_left >= params.min_flush_size
   then
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n params node_id_cnt msgs_left st
-    let (n2, node_id_cnt1) := p1
+      betree.Node.apply_messages self.left params node_id_cnt msgs_left st
+    let (n, node_id_cnt1) := p1
     let len_right ← betree.List.len (U64 × betree.Message) msgs_right
     if len_right >= params.min_flush_size
     then
       do
       let (st2, p2) ←
-        betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
-      let (n3, node_id_cnt2) := p2
-      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
-        node_id_cnt2)))
+        betree.Node.apply_messages self.right params node_id_cnt1 msgs_right
+          st1
+      let (n1, node_id_cnt2) := p2
+      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot
+        n n1, node_id_cnt2)))
     else
-      Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
-        node_id_cnt1)))
+      Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n
+        self.right, node_id_cnt1)))
   else
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n1 params node_id_cnt msgs_right st
-    let (n2, node_id_cnt1) := p1
-    Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+      betree.Node.apply_messages self.right params node_id_cnt msgs_right st
+    let (n, node_id_cnt1) := p1
+    Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot
+      self.left n, node_id_cnt1)))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
+/- [betree::betree::{betree::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
 divergent def betree.Node.apply_messages
   (self : betree.Node) (params : betree.Params)
@@ -581,26 +573,21 @@ divergent def betree.Node.apply_messages
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, content) ← betree.load_internal_node i st
+    let (st1, content) ← betree.load_internal_node node.id st
     let content1 ← betree.Node.apply_messages_to_internal content msgs
     let num_msgs ← betree.List.len (U64 × betree.Message) content1
     if num_msgs >= params.min_flush_size
     then
       do
       let (st2, (content2, p)) ←
-        betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
-          content1 st1
+        betree.Internal.flush node params node_id_cnt content1 st1
       let (node1, node_id_cnt1) := p
-      let ⟨ i2, i3, n2, n3 ⟩ := node1
-      let (st3, _) ← betree.store_internal_node i2 content2 st2
-      Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
-        node_id_cnt1))
+      let (st3, _) ← betree.store_internal_node node1.id content2 st2
+      Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_internal_node i content1 st1
-      Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
-        node_id_cnt))
+      let (st2, _) ← betree.store_internal_node node.id content1 st1
+      Result.ok (st2, (betree.Node.Internal node, node_id_cnt))
   | betree.Node.Leaf node =>
     do
     let (st1, content) ← betree.load_leaf_node node.id st
@@ -622,7 +609,7 @@ divergent def betree.Node.apply_messages
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]:
+/- [betree::betree::{betree::betree::Node#5}::apply]:
    Source: 'src/betree.rs', lines 576:4-582:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
@@ -637,7 +624,7 @@ def betree.Node.apply
   let (self1, node_id_cnt1) := p
   Result.ok (st1, (self1, node_id_cnt1))
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
+/- [betree::betree::{betree::betree::BeTree#6}::new]:
    Source: 'src/betree.rs', lines 849:4-849:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
@@ -654,7 +641,7 @@ def betree.BeTree.new
       root := (betree.Node.Leaf { id := id, size := 0#u64 })
     })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
+/- [betree::betree::{betree::betree::BeTree#6}::apply]:
    Source: 'src/betree.rs', lines 868:4-868:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
@@ -666,7 +653,7 @@ def betree.BeTree.apply
   let (n, nic) := p
   Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
+/- [betree::betree::{betree::betree::BeTree#6}::insert]:
    Source: 'src/betree.rs', lines 874:4-874:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
@@ -674,7 +661,7 @@ def betree.BeTree.insert
   :=
   betree.BeTree.apply self key (betree.Message.Insert value) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
+/- [betree::betree::{betree::betree::BeTree#6}::delete]:
    Source: 'src/betree.rs', lines 880:4-880:38 -/
 def betree.BeTree.delete
   (self : betree.BeTree) (key : U64) (st : State) :
@@ -682,7 +669,7 @@ def betree.BeTree.delete
   :=
   betree.BeTree.apply self key betree.Message.Delete st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
+/- [betree::betree::{betree::betree::BeTree#6}::upsert]:
    Source: 'src/betree.rs', lines 886:4-886:59 -/
 def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
@@ -691,7 +678,7 @@ def betree.BeTree.upsert
   :=
   betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
+/- [betree::betree::{betree::betree::BeTree#6}::lookup]:
    Source: 'src/betree.rs', lines 895:4-895:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
@@ -701,12 +688,12 @@ def betree.BeTree.lookup
   let (st1, (o, n)) ← betree.Node.lookup self.root key st
   Result.ok (st1, (o, { self with root := n }))
 
-/- [betree_main::main]:
+/- [betree::main]:
    Source: 'src/main.rs', lines 4:0-4:9 -/
 def main : Result Unit :=
   Result.ok ()
 
-/- Unit test for [betree_main::main] -/
+/- Unit test for [betree::main] -/
 #assert (main == Result.ok ())
 
-end betree_main
+end betree
diff --git a/tests/lean/BetreeMain/FunsExternal.lean b/tests/lean/Betree/FunsExternal.lean
index d26177fb..859cbd68 100644
--- a/tests/lean/BetreeMain/FunsExternal.lean
+++ b/tests/lean/Betree/FunsExternal.lean
@@ -1,30 +1,30 @@
--- [betree_main]: external functions.
+-- [betree]: external functions.
 import Base
-import BetreeMain.Types
+import Betree.Types
 open Primitives
-open betree_main
+open betree
 
 -- TODO: fill those bodies
 
-/- [betree_main::betree_utils::load_internal_node] -/
+/- [betree::betree_utils::load_internal_node] -/
 def betree_utils.load_internal_node
   :
   U64 → State → Result (State × (betree.List (U64 × betree.Message))) :=
   fun _ _ => .fail .panic
 
-/- [betree_main::betree_utils::store_internal_node] -/
+/- [betree::betree_utils::store_internal_node] -/
 def betree_utils.store_internal_node
   :
   U64 → betree.List (U64 × betree.Message) → State → Result (State
     × Unit) :=
   fun _ _ _ => .fail .panic
 
-/- [betree_main::betree_utils::load_leaf_node] -/
+/- [betree::betree_utils::load_leaf_node] -/
 def betree_utils.load_leaf_node
   : U64 → State → Result (State × (betree.List (U64 × U64))) :=
   fun _ _ => .fail .panic
 
-/- [betree_main::betree_utils::store_leaf_node] -/
+/- [betree::betree_utils::store_leaf_node] -/
 def betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit) :=
   fun _ _ _ => .fail .panic
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean
index 0dcce5ca..014f0d83 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/Betree/FunsExternal_Template.lean
@@ -1,29 +1,29 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: external functions.
+-- [betree]: external functions.
 -- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
 import Base
-import BetreeMain.Types
+import Betree.Types
 open Primitives
-open betree_main
+open betree
 
-/- [betree_main::betree_utils::load_internal_node]:
+/- [betree::betree_utils::load_internal_node]:
    Source: 'src/betree_utils.rs', lines 98:0-98:63 -/
 axiom betree_utils.load_internal_node
   : U64 → State → Result (State × (betree.List (U64 × betree.Message)))
 
-/- [betree_main::betree_utils::store_internal_node]:
+/- [betree::betree_utils::store_internal_node]:
    Source: 'src/betree_utils.rs', lines 115:0-115:71 -/
 axiom betree_utils.store_internal_node
   :
   U64 → betree.List (U64 × betree.Message) → State → Result (State ×
     Unit)
 
-/- [betree_main::betree_utils::load_leaf_node]:
+/- [betree::betree_utils::load_leaf_node]:
    Source: 'src/betree_utils.rs', lines 132:0-132:55 -/
 axiom betree_utils.load_leaf_node
   : U64 → State → Result (State × (betree.List (U64 × U64)))
 
-/- [betree_main::betree_utils::store_leaf_node]:
+/- [betree::betree_utils::store_leaf_node]:
    Source: 'src/betree_utils.rs', lines 145:0-145:63 -/
 axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/Betree/Types.lean
index 877508f6..3b46c00c 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/Betree/Types.lean
@@ -1,31 +1,31 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: type definitions
+-- [betree]: type definitions
 import Base
-import BetreeMain.TypesExternal
+import Betree.TypesExternal
 open Primitives
 
-namespace betree_main
+namespace betree
 
-/- [betree_main::betree::List]
+/- [betree::betree::List]
    Source: 'src/betree.rs', lines 17:0-17:23 -/
 inductive betree.List (T : Type) :=
 | Cons : T → betree.List T → betree.List T
 | Nil : betree.List T
 
-/- [betree_main::betree::UpsertFunState]
+/- [betree::betree::UpsertFunState]
    Source: 'src/betree.rs', lines 63:0-63:23 -/
 inductive betree.UpsertFunState :=
 | Add : U64 → betree.UpsertFunState
 | Sub : U64 → betree.UpsertFunState
 
-/- [betree_main::betree::Message]
+/- [betree::betree::Message]
    Source: 'src/betree.rs', lines 69:0-69:23 -/
 inductive betree.Message :=
 | Insert : U64 → betree.Message
 | Delete : betree.Message
 | Upsert : betree.UpsertFunState → betree.Message
 
-/- [betree_main::betree::Leaf]
+/- [betree::betree::Leaf]
    Source: 'src/betree.rs', lines 167:0-167:11 -/
 structure betree.Leaf where
   id : U64
@@ -33,12 +33,12 @@ structure betree.Leaf where
 
 mutual
 
-/- [betree_main::betree::Internal]
+/- [betree::betree::Internal]
    Source: 'src/betree.rs', lines 156:0-156:15 -/
 inductive betree.Internal :=
 | mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
 
-/- [betree_main::betree::Node]
+/- [betree::betree::Node]
    Source: 'src/betree.rs', lines 179:0-179:9 -/
 inductive betree.Node :=
 | Internal : betree.Internal → betree.Node
@@ -46,22 +46,38 @@ inductive betree.Node :=
 
 end
 
-/- [betree_main::betree::Params]
+@[simp, reducible]
+def betree.Internal.id (x : betree.Internal) :=
+  match x with | betree.Internal.mk x1 _ _ _ => x1
+
+@[simp, reducible]
+def betree.Internal.pivot (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ x1 _ _ => x1
+
+@[simp, reducible]
+def betree.Internal.left (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ x1 _ => x1
+
+@[simp, reducible]
+def betree.Internal.right (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ _ x1 => x1
+
+/- [betree::betree::Params]
    Source: 'src/betree.rs', lines 187:0-187:13 -/
 structure betree.Params where
   min_flush_size : U64
   split_size : U64
 
-/- [betree_main::betree::NodeIdCounter]
+/- [betree::betree::NodeIdCounter]
    Source: 'src/betree.rs', lines 201:0-201:20 -/
 structure betree.NodeIdCounter where
   next_node_id : U64
 
-/- [betree_main::betree::BeTree]
+/- [betree::betree::BeTree]
    Source: 'src/betree.rs', lines 218:0-218:17 -/
 structure betree.BeTree where
   params : betree.Params
   node_id_cnt : betree.NodeIdCounter
   root : betree.Node
 
-end betree_main
+end betree
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/Betree/TypesExternal.lean
index 1701eaaf..34170271 100644
--- a/tests/lean/BetreeMain/TypesExternal.lean
+++ b/tests/lean/Betree/TypesExternal.lean
@@ -1,4 +1,4 @@
--- [betree_main]: external types.
+-- [betree]: external types.
 import Base
 open Primitives
 
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean
index bbac7e99..12fce657 100644
--- a/tests/lean/BetreeMain/TypesExternal_Template.lean
+++ b/tests/lean/Betree/TypesExternal_Template.lean
@@ -1,5 +1,5 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [betree_main]: external types.
+-- [betree]: external types.
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
diff --git a/tests/lean/BetreeMain.lean b/tests/lean/BetreeMain.lean
deleted file mode 100644
index 5f307877..00000000
--- a/tests/lean/BetreeMain.lean
+++ /dev/null
@@ -1 +0,0 @@
-import BetreeMain.Funs
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 4ed56a0a..23ec66b4 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -6,31 +6,31 @@ open Primitives
 namespace bitwise
 
 /- [bitwise::shift_u32]:
-   Source: 'tests/src/bitwise.rs', lines 3:0-3:31 -/
+   Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/
 def shift_u32 (a : U32) : Result U32 :=
   do
   let t ← a >>> 16#usize
   t <<< 16#usize
 
 /- [bitwise::shift_i32]:
-   Source: 'tests/src/bitwise.rs', lines 10:0-10:31 -/
+   Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
 def shift_i32 (a : I32) : Result I32 :=
   do
   let t ← a >>> 16#isize
   t <<< 16#isize
 
 /- [bitwise::xor_u32]:
-   Source: 'tests/src/bitwise.rs', lines 17:0-17:37 -/
+   Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/
 def xor_u32 (a : U32) (b : U32) : Result U32 :=
   Result.ok (a ^^^ b)
 
 /- [bitwise::or_u32]:
-   Source: 'tests/src/bitwise.rs', lines 21:0-21:36 -/
+   Source: 'tests/src/bitwise.rs', lines 23:0-23:36 -/
 def or_u32 (a : U32) (b : U32) : Result U32 :=
   Result.ok (a ||| b)
 
 /- [bitwise::and_u32]:
-   Source: 'tests/src/bitwise.rs', lines 25:0-25:37 -/
+   Source: 'tests/src/bitwise.rs', lines 27:0-27:37 -/
 def and_u32 (a : U32) (b : U32) : Result U32 :=
   Result.ok (a &&& b)
 
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 532f265a..ecb91c16 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -6,123 +6,123 @@ open Primitives
 namespace constants
 
 /- [constants::X0]
-   Source: 'tests/src/constants.rs', lines 5:0-5:17 -/
+   Source: 'tests/src/constants.rs', lines 8:0-8:17 -/
 def X0_body : Result U32 := Result.ok 0#u32
 def X0 : U32 := eval_global X0_body
 
 /- [constants::X1]
-   Source: 'tests/src/constants.rs', lines 7:0-7:17 -/
+   Source: 'tests/src/constants.rs', lines 10:0-10:17 -/
 def X1_body : Result U32 := Result.ok core_u32_max
 def X1 : U32 := eval_global X1_body
 
 /- [constants::X2]
-   Source: 'tests/src/constants.rs', lines 10:0-10:17 -/
+   Source: 'tests/src/constants.rs', lines 13:0-13:17 -/
 def X2_body : Result U32 := Result.ok 3#u32
 def X2 : U32 := eval_global X2_body
 
 /- [constants::incr]:
-   Source: 'tests/src/constants.rs', lines 17:0-17:32 -/
+   Source: 'tests/src/constants.rs', lines 20:0-20:32 -/
 def incr (n : U32) : Result U32 :=
   n + 1#u32
 
 /- [constants::X3]
-   Source: 'tests/src/constants.rs', lines 15:0-15:17 -/
+   Source: 'tests/src/constants.rs', lines 18:0-18:17 -/
 def X3_body : Result U32 := incr 32#u32
 def X3 : U32 := eval_global X3_body
 
 /- [constants::mk_pair0]:
-   Source: 'tests/src/constants.rs', lines 23:0-23:51 -/
+   Source: 'tests/src/constants.rs', lines 26:0-26:51 -/
 def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) :=
   Result.ok (x, y)
 
 /- [constants::Pair]
-   Source: 'tests/src/constants.rs', lines 36:0-36:23 -/
+   Source: 'tests/src/constants.rs', lines 39:0-39:23 -/
 structure Pair (T1 T2 : Type) where
   x : T1
   y : T2
 
 /- [constants::mk_pair1]:
-   Source: 'tests/src/constants.rs', lines 27:0-27:55 -/
+   Source: 'tests/src/constants.rs', lines 30:0-30:55 -/
 def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
   Result.ok { x := x, y := y }
 
 /- [constants::P0]
-   Source: 'tests/src/constants.rs', lines 31:0-31:24 -/
+   Source: 'tests/src/constants.rs', lines 34:0-34:24 -/
 def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32
 def P0 : (U32 × U32) := eval_global P0_body
 
 /- [constants::P1]
-   Source: 'tests/src/constants.rs', lines 32:0-32:28 -/
+   Source: 'tests/src/constants.rs', lines 35:0-35:28 -/
 def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32
 def P1 : Pair U32 U32 := eval_global P1_body
 
 /- [constants::P2]
-   Source: 'tests/src/constants.rs', lines 33:0-33:24 -/
+   Source: 'tests/src/constants.rs', lines 36:0-36:24 -/
 def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32)
 def P2 : (U32 × U32) := eval_global P2_body
 
 /- [constants::P3]
-   Source: 'tests/src/constants.rs', lines 34:0-34:28 -/
+   Source: 'tests/src/constants.rs', lines 37:0-37:28 -/
 def P3_body : Result (Pair U32 U32) := Result.ok { x := 0#u32, y := 1#u32 }
 def P3 : Pair U32 U32 := eval_global P3_body
 
 /- [constants::Wrap]
-   Source: 'tests/src/constants.rs', lines 49:0-49:18 -/
+   Source: 'tests/src/constants.rs', lines 52:0-52:18 -/
 structure Wrap (T : Type) where
   value : T
 
 /- [constants::{constants::Wrap<T>}::new]:
-   Source: 'tests/src/constants.rs', lines 54:4-54:41 -/
+   Source: 'tests/src/constants.rs', lines 57:4-57:41 -/
 def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
   Result.ok { value := value }
 
 /- [constants::Y]
-   Source: 'tests/src/constants.rs', lines 41:0-41:22 -/
+   Source: 'tests/src/constants.rs', lines 44:0-44:22 -/
 def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32
 def Y : Wrap I32 := eval_global Y_body
 
 /- [constants::unwrap_y]:
-   Source: 'tests/src/constants.rs', lines 43:0-43:30 -/
+   Source: 'tests/src/constants.rs', lines 46:0-46:30 -/
 def unwrap_y : Result I32 :=
   Result.ok Y.value
 
 /- [constants::YVAL]
-   Source: 'tests/src/constants.rs', lines 47:0-47:19 -/
+   Source: 'tests/src/constants.rs', lines 50:0-50:19 -/
 def YVAL_body : Result I32 := unwrap_y
 def YVAL : I32 := eval_global YVAL_body
 
 /- [constants::get_z1::Z1]
-   Source: 'tests/src/constants.rs', lines 62:4-62:17 -/
+   Source: 'tests/src/constants.rs', lines 65:4-65:17 -/
 def get_z1.Z1_body : Result I32 := Result.ok 3#i32
 def get_z1.Z1 : I32 := eval_global get_z1.Z1_body
 
 /- [constants::get_z1]:
-   Source: 'tests/src/constants.rs', lines 61:0-61:28 -/
+   Source: 'tests/src/constants.rs', lines 64:0-64:28 -/
 def get_z1 : Result I32 :=
   Result.ok get_z1.Z1
 
 /- [constants::add]:
-   Source: 'tests/src/constants.rs', lines 66:0-66:39 -/
+   Source: 'tests/src/constants.rs', lines 69:0-69:39 -/
 def add (a : I32) (b : I32) : Result I32 :=
   a + b
 
 /- [constants::Q1]
-   Source: 'tests/src/constants.rs', lines 74:0-74:17 -/
+   Source: 'tests/src/constants.rs', lines 77:0-77:17 -/
 def Q1_body : Result I32 := Result.ok 5#i32
 def Q1 : I32 := eval_global Q1_body
 
 /- [constants::Q2]
-   Source: 'tests/src/constants.rs', lines 75:0-75:17 -/
+   Source: 'tests/src/constants.rs', lines 78:0-78:17 -/
 def Q2_body : Result I32 := Result.ok Q1
 def Q2 : I32 := eval_global Q2_body
 
 /- [constants::Q3]
-   Source: 'tests/src/constants.rs', lines 76:0-76:17 -/
+   Source: 'tests/src/constants.rs', lines 79:0-79:17 -/
 def Q3_body : Result I32 := add Q2 3#i32
 def Q3 : I32 := eval_global Q3_body
 
 /- [constants::get_z2]:
-   Source: 'tests/src/constants.rs', lines 70:0-70:28 -/
+   Source: 'tests/src/constants.rs', lines 73:0-73:28 -/
 def get_z2 : Result I32 :=
   do
   let i ← get_z1
@@ -130,37 +130,37 @@ def get_z2 : Result I32 :=
   add Q1 i1
 
 /- [constants::S1]
-   Source: 'tests/src/constants.rs', lines 80:0-80:18 -/
+   Source: 'tests/src/constants.rs', lines 83:0-83:18 -/
 def S1_body : Result U32 := Result.ok 6#u32
 def S1 : U32 := eval_global S1_body
 
 /- [constants::S2]
-   Source: 'tests/src/constants.rs', lines 81:0-81:18 -/
+   Source: 'tests/src/constants.rs', lines 84:0-84:18 -/
 def S2_body : Result U32 := incr S1
 def S2 : U32 := eval_global S2_body
 
 /- [constants::S3]
-   Source: 'tests/src/constants.rs', lines 82:0-82:29 -/
+   Source: 'tests/src/constants.rs', lines 85:0-85:29 -/
 def S3_body : Result (Pair U32 U32) := Result.ok P3
 def S3 : Pair U32 U32 := eval_global S3_body
 
 /- [constants::S4]
-   Source: 'tests/src/constants.rs', lines 83:0-83:29 -/
+   Source: 'tests/src/constants.rs', lines 86:0-86:29 -/
 def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
 def S4 : Pair U32 U32 := eval_global S4_body
 
 /- [constants::V]
-   Source: 'tests/src/constants.rs', lines 86:0-86:31 -/
+   Source: 'tests/src/constants.rs', lines 89:0-89:31 -/
 structure V (T : Type) (N : Usize) where
   x : Array T N
 
 /- [constants::{constants::V<T, N>#1}::LEN]
-   Source: 'tests/src/constants.rs', lines 91:4-91:24 -/
+   Source: 'tests/src/constants.rs', lines 94:4-94:24 -/
 def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
 def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N)
 
 /- [constants::use_v]:
-   Source: 'tests/src/constants.rs', lines 94:0-94:42 -/
+   Source: 'tests/src/constants.rs', lines 97:0-97:42 -/
 def use_v (T : Type) (N : Usize) : Result Usize :=
   Result.ok (V.LEN T N)
 
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index a9b349b3..48ac2062 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -6,7 +6,7 @@ open Primitives
 namespace demo
 
 /- [demo::choose]:
-   Source: 'tests/src/demo.rs', lines 5:0-5:70 -/
+   Source: 'tests/src/demo.rs', lines 7:0-7:70 -/
 def choose
   (T : Type) (b : Bool) (x : T) (y : T) :
   Result (T × (T → Result (T × T)))
@@ -18,26 +18,26 @@ def choose
        Result.ok (y, back)
 
 /- [demo::mul2_add1]:
-   Source: 'tests/src/demo.rs', lines 13:0-13:31 -/
+   Source: 'tests/src/demo.rs', lines 15:0-15:31 -/
 def mul2_add1 (x : U32) : Result U32 :=
   do
   let i ← x + x
   i + 1#u32
 
 /- [demo::use_mul2_add1]:
-   Source: 'tests/src/demo.rs', lines 17:0-17:43 -/
+   Source: 'tests/src/demo.rs', lines 19:0-19:43 -/
 def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
   do
   let i ← mul2_add1 x
   i + y
 
 /- [demo::incr]:
-   Source: 'tests/src/demo.rs', lines 21:0-21:31 -/
+   Source: 'tests/src/demo.rs', lines 23:0-23:31 -/
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
 /- [demo::use_incr]:
-   Source: 'tests/src/demo.rs', lines 25:0-25:17 -/
+   Source: 'tests/src/demo.rs', lines 27:0-27:17 -/
 def use_incr : Result Unit :=
   do
   let x ← incr 0#u32
@@ -46,13 +46,13 @@ def use_incr : Result Unit :=
   Result.ok ()
 
 /- [demo::CList]
-   Source: 'tests/src/demo.rs', lines 34:0-34:17 -/
+   Source: 'tests/src/demo.rs', lines 36:0-36:17 -/
 inductive CList (T : Type) :=
 | CCons : T → CList T → CList T
 | CNil : CList T
 
 /- [demo::list_nth]:
-   Source: 'tests/src/demo.rs', lines 39:0-39:56 -/
+   Source: 'tests/src/demo.rs', lines 41:0-41:56 -/
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
@@ -64,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut]:
-   Source: 'tests/src/demo.rs', lines 54:0-54:68 -/
+   Source: 'tests/src/demo.rs', lines 56:0-56:68 -/
 divergent def list_nth_mut
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -88,7 +88,7 @@ divergent def list_nth_mut
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
-   Source: 'tests/src/demo.rs', lines 69:0-78:1 -/
+   Source: 'tests/src/demo.rs', lines 71:0-80:1 -/
 divergent def list_nth_mut1_loop
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -111,7 +111,7 @@ divergent def list_nth_mut1_loop
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
-   Source: 'tests/src/demo.rs', lines 69:0-69:77 -/
+   Source: 'tests/src/demo.rs', lines 71:0-71:77 -/
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -119,7 +119,7 @@ def list_nth_mut1
   list_nth_mut1_loop T l i
 
 /- [demo::i32_id]:
-   Source: 'tests/src/demo.rs', lines 80:0-80:28 -/
+   Source: 'tests/src/demo.rs', lines 82:0-82:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
   then Result.ok 0#i32
@@ -129,7 +129,7 @@ divergent def i32_id (i : I32) : Result I32 :=
        i2 + 1#i32
 
 /- [demo::list_tail]:
-   Source: 'tests/src/demo.rs', lines 88:0-88:64 -/
+   Source: 'tests/src/demo.rs', lines 90:0-90:64 -/
 divergent def list_tail
   (T : Type) (l : CList T) :
   Result ((CList T) × (CList T → Result (CList T)))
@@ -147,25 +147,25 @@ divergent def list_tail
   | CList.CNil => Result.ok (CList.CNil, Result.ok)
 
 /- Trait declaration: [demo::Counter]
-   Source: 'tests/src/demo.rs', lines 97:0-97:17 -/
+   Source: 'tests/src/demo.rs', lines 99:0-99:17 -/
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
 /- [demo::{(demo::Counter for usize)}::incr]:
-   Source: 'tests/src/demo.rs', lines 102:4-102:31 -/
+   Source: 'tests/src/demo.rs', lines 104:4-104:31 -/
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ok (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
-   Source: 'tests/src/demo.rs', lines 101:0-101:22 -/
+   Source: 'tests/src/demo.rs', lines 103:0-103:22 -/
 def CounterUsize : Counter Usize := {
   incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
-   Source: 'tests/src/demo.rs', lines 109:0-109:59 -/
+   Source: 'tests/src/demo.rs', lines 111:0-111:59 -/
 def use_counter
   (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
   CounterInst.incr cnt
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 5e3c9b1d..1acb9707 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -15,12 +15,12 @@ def core.marker.CopyU32 : core.marker.Copy U32 := {
 }
 
 /- [external::use_get]:
-   Source: 'tests/src/external.rs', lines 5:0-5:37 -/
+   Source: 'tests/src/external.rs', lines 9:0-9:37 -/
 def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
   core.cell.Cell.get U32 core.marker.CopyU32 rc st
 
 /- [external::incr]:
-   Source: 'tests/src/external.rs', lines 9:0-9:31 -/
+   Source: 'tests/src/external.rs', lines 13:0-13:31 -/
 def incr
   (rc : core.cell.Cell U32) (st : State) :
   Result (State × (core.cell.Cell U32))
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index cb11e5cf..d7ac3b05 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -2,17 +2,18 @@
 -- [hashmap]: function definitions
 import Base
 import Hashmap.Types
+import Hashmap.FunsExternal
 open Primitives
 
 namespace hashmap
 
 /- [hashmap::hash_key]:
-   Source: 'tests/src/hashmap.rs', lines 27:0-27:32 -/
+   Source: 'tests/src/hashmap.rs', lines 37:0-37:32 -/
 def hash_key (k : Usize) : Result Usize :=
   Result.ok k
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 50:4-56:5 -/
+   Source: 'tests/src/hashmap.rs', lines 60:4-66:5 -/
 divergent def HashMap.allocate_slots_loop
   (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
   Result (alloc.vec.Vec (List T))
@@ -26,7 +27,7 @@ divergent def HashMap.allocate_slots_loop
   else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
-   Source: 'tests/src/hashmap.rs', lines 50:4-50:76 -/
+   Source: 'tests/src/hashmap.rs', lines 60:4-60:76 -/
 def HashMap.allocate_slots
   (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
   Result (alloc.vec.Vec (List T))
@@ -34,7 +35,7 @@ def HashMap.allocate_slots
   HashMap.allocate_slots_loop T slots n
 
 /- [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
-   Source: 'tests/src/hashmap.rs', lines 59:4-63:13 -/
+   Source: 'tests/src/hashmap.rs', lines 69:4-73:13 -/
 def HashMap.new_with_capacity
   (T : Type) (capacity : Usize) (max_load_dividend : Usize)
   (max_load_divisor : Usize) :
@@ -53,12 +54,12 @@ def HashMap.new_with_capacity
     }
 
 /- [hashmap::{hashmap::HashMap<T>}::new]:
-   Source: 'tests/src/hashmap.rs', lines 75:4-75:24 -/
+   Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/
 def HashMap.new (T : Type) : Result (HashMap T) :=
   HashMap.new_with_capacity T 32#usize 4#usize 5#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 80:4-88:5 -/
+   Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/
 divergent def HashMap.clear_loop
   (T : Type) (slots : alloc.vec.Vec (List T)) (i : Usize) :
   Result (alloc.vec.Vec (List T))
@@ -76,19 +77,19 @@ divergent def HashMap.clear_loop
   else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]:
-   Source: 'tests/src/hashmap.rs', lines 80:4-80:27 -/
+   Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
   let hm ← HashMap.clear_loop T self.slots 0#usize
   Result.ok { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap::{hashmap::HashMap<T>}::len]:
-   Source: 'tests/src/hashmap.rs', lines 90:4-90:30 -/
+   Source: 'tests/src/hashmap.rs', lines 100:4-100:30 -/
 def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
   Result.ok self.num_entries
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 97:4-114:5 -/
+   Source: 'tests/src/hashmap.rs', lines 107:4-124:5 -/
 divergent def HashMap.insert_in_list_loop
   (T : Type) (key : Usize) (value : T) (ls : List T) :
   Result (Bool × (List T))
@@ -104,7 +105,7 @@ divergent def HashMap.insert_in_list_loop
   | List.Nil => Result.ok (true, List.Cons key value List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 97:4-97:71 -/
+   Source: 'tests/src/hashmap.rs', lines 107:4-107:71 -/
 def HashMap.insert_in_list
   (T : Type) (key : Usize) (value : T) (ls : List T) :
   Result (Bool × (List T))
@@ -112,7 +113,7 @@ def HashMap.insert_in_list
   HashMap.insert_in_list_loop T key value ls
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
-   Source: 'tests/src/hashmap.rs', lines 117:4-117:54 -/
+   Source: 'tests/src/hashmap.rs', lines 127:4-127:54 -/
 def HashMap.insert_no_resize
   (T : Type) (self : HashMap T) (key : Usize) (value : T) :
   Result (HashMap T)
@@ -136,7 +137,7 @@ def HashMap.insert_no_resize
        Result.ok { self with slots := v }
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 183:4-196:5 -/
+   Source: 'tests/src/hashmap.rs', lines 193:4-206:5 -/
 divergent def HashMap.move_elements_from_list_loop
   (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) :=
   match ls with
@@ -147,13 +148,13 @@ divergent def HashMap.move_elements_from_list_loop
   | List.Nil => Result.ok ntable
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
-   Source: 'tests/src/hashmap.rs', lines 183:4-183:72 -/
+   Source: 'tests/src/hashmap.rs', lines 193:4-193:72 -/
 def HashMap.move_elements_from_list
   (T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) :=
   HashMap.move_elements_from_list_loop T ntable ls
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 171:4-180:5 -/
+   Source: 'tests/src/hashmap.rs', lines 181:4-190:5 -/
 divergent def HashMap.move_elements_loop
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize)
   :
@@ -174,7 +175,7 @@ divergent def HashMap.move_elements_loop
   else Result.ok (ntable, slots)
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
-   Source: 'tests/src/hashmap.rs', lines 171:4-171:95 -/
+   Source: 'tests/src/hashmap.rs', lines 181:4-181:95 -/
 def HashMap.move_elements
   (T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize)
   :
@@ -183,7 +184,7 @@ def HashMap.move_elements
   HashMap.move_elements_loop T ntable slots i
 
 /- [hashmap::{hashmap::HashMap<T>}::try_resize]:
-   Source: 'tests/src/hashmap.rs', lines 140:4-140:28 -/
+   Source: 'tests/src/hashmap.rs', lines 150:4-150:28 -/
 def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
   let max_usize ← Scalar.cast .Usize core_u32_max
@@ -207,7 +208,7 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   else Result.ok { self with max_load_factor := (i, i1) }
 
 /- [hashmap::{hashmap::HashMap<T>}::insert]:
-   Source: 'tests/src/hashmap.rs', lines 129:4-129:48 -/
+   Source: 'tests/src/hashmap.rs', lines 139:4-139:48 -/
 def HashMap.insert
   (T : Type) (self : HashMap T) (key : Usize) (value : T) :
   Result (HashMap T)
@@ -220,7 +221,7 @@ def HashMap.insert
   else Result.ok self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 206:4-219:5 -/
+   Source: 'tests/src/hashmap.rs', lines 216:4-229:5 -/
 divergent def HashMap.contains_key_in_list_loop
   (T : Type) (key : Usize) (ls : List T) : Result Bool :=
   match ls with
@@ -231,13 +232,13 @@ divergent def HashMap.contains_key_in_list_loop
   | List.Nil => Result.ok false
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 206:4-206:68 -/
+   Source: 'tests/src/hashmap.rs', lines 216:4-216:68 -/
 def HashMap.contains_key_in_list
   (T : Type) (key : Usize) (ls : List T) : Result Bool :=
   HashMap.contains_key_in_list_loop T key ls
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key]:
-   Source: 'tests/src/hashmap.rs', lines 199:4-199:49 -/
+   Source: 'tests/src/hashmap.rs', lines 209:4-209:49 -/
 def HashMap.contains_key
   (T : Type) (self : HashMap T) (key : Usize) : Result Bool :=
   do
@@ -250,7 +251,7 @@ def HashMap.contains_key
   HashMap.contains_key_in_list T key l
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 224:4-237:5 -/
+   Source: 'tests/src/hashmap.rs', lines 234:4-247:5 -/
 divergent def HashMap.get_in_list_loop
   (T : Type) (key : Usize) (ls : List T) : Result T :=
   match ls with
@@ -261,12 +262,12 @@ divergent def HashMap.get_in_list_loop
   | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 224:4-224:70 -/
+   Source: 'tests/src/hashmap.rs', lines 234:4-234:70 -/
 def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T :=
   HashMap.get_in_list_loop T key ls
 
 /- [hashmap::{hashmap::HashMap<T>}::get]:
-   Source: 'tests/src/hashmap.rs', lines 239:4-239:55 -/
+   Source: 'tests/src/hashmap.rs', lines 249:4-249:55 -/
 def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
   do
   let hash ← hash_key key
@@ -278,7 +279,7 @@ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
   HashMap.get_in_list T key l
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 245:4-254:5 -/
+   Source: 'tests/src/hashmap.rs', lines 255:4-264:5 -/
 divergent def HashMap.get_mut_in_list_loop
   (T : Type) (ls : List T) (key : Usize) :
   Result (T × (T → Result (List T)))
@@ -301,7 +302,7 @@ divergent def HashMap.get_mut_in_list_loop
   | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 245:4-245:86 -/
+   Source: 'tests/src/hashmap.rs', lines 255:4-255:86 -/
 def HashMap.get_mut_in_list
   (T : Type) (ls : List T) (key : Usize) :
   Result (T × (T → Result (List T)))
@@ -309,7 +310,7 @@ def HashMap.get_mut_in_list
   HashMap.get_mut_in_list_loop T ls key
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut]:
-   Source: 'tests/src/hashmap.rs', lines 257:4-257:67 -/
+   Source: 'tests/src/hashmap.rs', lines 267:4-267:67 -/
 def HashMap.get_mut
   (T : Type) (self : HashMap T) (key : Usize) :
   Result (T × (T → Result (HashMap T)))
@@ -331,7 +332,7 @@ def HashMap.get_mut
   Result.ok (t, back)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 265:4-291:5 -/
+   Source: 'tests/src/hashmap.rs', lines 275:4-301:5 -/
 divergent def HashMap.remove_from_list_loop
   (T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) :=
   match ls with
@@ -350,13 +351,13 @@ divergent def HashMap.remove_from_list_loop
   | List.Nil => Result.ok (none, List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
-   Source: 'tests/src/hashmap.rs', lines 265:4-265:69 -/
+   Source: 'tests/src/hashmap.rs', lines 275:4-275:69 -/
 def HashMap.remove_from_list
   (T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) :=
   HashMap.remove_from_list_loop T key ls
 
 /- [hashmap::{hashmap::HashMap<T>}::remove]:
-   Source: 'tests/src/hashmap.rs', lines 294:4-294:52 -/
+   Source: 'tests/src/hashmap.rs', lines 304:4-304:52 -/
 def HashMap.remove
   (T : Type) (self : HashMap T) (key : Usize) :
   Result ((Option T) × (HashMap T))
@@ -380,8 +381,17 @@ def HashMap.remove
     let v ← index_mut_back l1
     Result.ok (some x1, { self with num_entries := i1, slots := v })
 
+/- [hashmap::insert_on_disk]:
+   Source: 'tests/src/hashmap.rs', lines 335:0-335:43 -/
+def insert_on_disk
+  (key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
+  do
+  let (st1, hm) ← utils.deserialize st
+  let hm1 ← HashMap.insert U64 hm key value
+  utils.serialize hm1 st1
+
 /- [hashmap::test1]:
-   Source: 'tests/src/hashmap.rs', lines 315:0-315:10 -/
+   Source: 'tests/src/hashmap.rs', lines 350:0-350:10 -/
 def test1 : Result Unit :=
   do
   let hm ← HashMap.new U64
diff --git a/tests/lean/Hashmap/FunsExternal.lean b/tests/lean/Hashmap/FunsExternal.lean
new file mode 100644
index 00000000..329e5d82
--- /dev/null
+++ b/tests/lean/Hashmap/FunsExternal.lean
@@ -0,0 +1,19 @@
+-- [hashmap]: external functions.
+import Base
+import Hashmap.Types
+open Primitives
+open hashmap
+
+-- TODO: fill those bodies
+
+/- [hashmap::utils::deserialize]:
+   Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
+def utils.deserialize
+  : State → Result (State × (HashMap U64)) :=
+  fun _ => .fail .panic
+
+/- [hashmap::utils::serialize]:
+   Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
+def utils.serialize
+  : HashMap U64 → State → Result (State × Unit) :=
+  fun _ _ => .fail .panic
diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean
new file mode 100644
index 00000000..2af57d10
--- /dev/null
+++ b/tests/lean/Hashmap/FunsExternal_Template.lean
@@ -0,0 +1,16 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Base
+import Hashmap.Types
+open Primitives
+open hashmap
+
+/- [hashmap::utils::deserialize]:
+   Source: 'tests/src/hashmap.rs', lines 330:4-330:47 -/
+axiom utils.deserialize : State → Result (State × (HashMap U64))
+
+/- [hashmap::utils::serialize]:
+   Source: 'tests/src/hashmap.rs', lines 325:4-325:46 -/
+axiom utils.serialize : HashMap U64 → State → Result (State × Unit)
+
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index c99ba8d0..b4301106 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -1,18 +1,19 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [hashmap]: type definitions
 import Base
+import Hashmap.TypesExternal
 open Primitives
 
 namespace hashmap
 
 /- [hashmap::List]
-   Source: 'tests/src/hashmap.rs', lines 19:0-19:16 -/
+   Source: 'tests/src/hashmap.rs', lines 29:0-29:16 -/
 inductive List (T : Type) :=
 | Cons : Usize → T → List T → List T
 | Nil : List T
 
 /- [hashmap::HashMap]
-   Source: 'tests/src/hashmap.rs', lines 35:0-35:21 -/
+   Source: 'tests/src/hashmap.rs', lines 45:0-45:21 -/
 structure HashMap (T : Type) where
   num_entries : Usize
   max_load_factor : (Usize × Usize)
diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/Hashmap/TypesExternal.lean
index 4e1cdbe9..b32c4c42 100644
--- a/tests/lean/HashmapMain/TypesExternal.lean
+++ b/tests/lean/Hashmap/TypesExternal.lean
@@ -1,4 +1,4 @@
--- [hashmap_main]: external types.
+-- [hashmap]: external types.
 import Base
 open Primitives
 
diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean
index cfa8bbb1..03c3d157 100644
--- a/tests/lean/HashmapMain/TypesExternal_Template.lean
+++ b/tests/lean/Hashmap/TypesExternal_Template.lean
@@ -1,5 +1,5 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [hashmap_main]: external types.
+-- [hashmap]: external types.
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
diff --git a/tests/lean/HashmapMain.lean b/tests/lean/HashmapMain.lean
deleted file mode 100644
index 1a4e7f82..00000000
--- a/tests/lean/HashmapMain.lean
+++ /dev/null
@@ -1 +0,0 @@
-import HashmapMain.Funs
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
deleted file mode 100644
index e27305b1..00000000
--- a/tests/lean/HashmapMain/Funs.lean
+++ /dev/null
@@ -1,463 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [hashmap_main]: function definitions
-import Base
-import HashmapMain.Types
-import HashmapMain.FunsExternal
-open Primitives
-
-namespace hashmap_main
-
-/- [hashmap_main::hashmap::hash_key]:
-   Source: 'tests/src/hashmap.rs', lines 27:0-27:32 -/
-def hashmap.hash_key (k : Usize) : Result Usize :=
-  Result.ok k
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 50:4-56:5 -/
-divergent def hashmap.HashMap.allocate_slots_loop
-  (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
-  Result (alloc.vec.Vec (hashmap.List T))
-  :=
-  if n > 0#usize
-  then
-    do
-    let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
-    let n1 ← n - 1#usize
-    hashmap.HashMap.allocate_slots_loop T slots1 n1
-  else Result.ok slots
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
-   Source: 'tests/src/hashmap.rs', lines 50:4-50:76 -/
-def hashmap.HashMap.allocate_slots
-  (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
-  Result (alloc.vec.Vec (hashmap.List T))
-  :=
-  hashmap.HashMap.allocate_slots_loop T slots n
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]:
-   Source: 'tests/src/hashmap.rs', lines 59:4-63:13 -/
-def hashmap.HashMap.new_with_capacity
-  (T : Type) (capacity : Usize) (max_load_dividend : Usize)
-  (max_load_divisor : Usize) :
-  Result (hashmap.HashMap T)
-  :=
-  do
-  let slots ←
-    hashmap.HashMap.allocate_slots T (alloc.vec.Vec.new (hashmap.List T))
-      capacity
-  let i ← capacity * max_load_dividend
-  let i1 ← i / max_load_divisor
-  Result.ok
-    {
-      num_entries := 0#usize,
-      max_load_factor := (max_load_dividend, max_load_divisor),
-      max_load := i1,
-      slots := slots
-    }
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]:
-   Source: 'tests/src/hashmap.rs', lines 75:4-75:24 -/
-def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) :=
-  hashmap.HashMap.new_with_capacity T 32#usize 4#usize 5#usize
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 80:4-88:5 -/
-divergent def hashmap.HashMap.clear_loop
-  (T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
-  Result (alloc.vec.Vec (hashmap.List T))
-  :=
-  let i1 := alloc.vec.Vec.len (hashmap.List T) slots
-  if i < i1
-  then
-    do
-    let (_, index_mut_back) ←
-      alloc.vec.Vec.index_mut (hashmap.List T) Usize
-        (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i
-    let i2 ← i + 1#usize
-    let slots1 ← index_mut_back hashmap.List.Nil
-    hashmap.HashMap.clear_loop T slots1 i2
-  else Result.ok slots
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]:
-   Source: 'tests/src/hashmap.rs', lines 80:4-80:27 -/
-def hashmap.HashMap.clear
-  (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
-  do
-  let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
-  Result.ok { self with num_entries := 0#usize, slots := hm }
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
-   Source: 'tests/src/hashmap.rs', lines 90:4-90:30 -/
-def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
-  Result.ok self.num_entries
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 97:4-114:5 -/
-divergent def hashmap.HashMap.insert_in_list_loop
-  (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) :
-  Result (Bool × (hashmap.List T))
-  :=
-  match ls with
-  | hashmap.List.Cons ckey cvalue tl =>
-    if ckey = key
-    then Result.ok (false, hashmap.List.Cons ckey value tl)
-    else
-      do
-      let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
-      Result.ok (b, hashmap.List.Cons ckey cvalue tl1)
-  | hashmap.List.Nil =>
-    Result.ok (true, hashmap.List.Cons key value hashmap.List.Nil)
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 97:4-97:71 -/
-def hashmap.HashMap.insert_in_list
-  (T : Type) (key : Usize) (value : T) (ls : hashmap.List T) :
-  Result (Bool × (hashmap.List T))
-  :=
-  hashmap.HashMap.insert_in_list_loop T key value ls
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]:
-   Source: 'tests/src/hashmap.rs', lines 117:4-117:54 -/
-def hashmap.HashMap.insert_no_resize
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) :
-  Result (hashmap.HashMap T)
-  :=
-  do
-  let hash ← hashmap.hash_key key
-  let i := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let hash_mod ← hash % i
-  let (l, index_mut_back) ←
-    alloc.vec.Vec.index_mut (hashmap.List T) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
-      hash_mod
-  let (inserted, l1) ← hashmap.HashMap.insert_in_list T key value l
-  if inserted
-  then
-    do
-    let i1 ← self.num_entries + 1#usize
-    let v ← index_mut_back l1
-    Result.ok { self with num_entries := i1, slots := v }
-  else do
-       let v ← index_mut_back l1
-       Result.ok { self with slots := v }
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 183:4-196:5 -/
-divergent def hashmap.HashMap.move_elements_from_list_loop
-  (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) :
-  Result (hashmap.HashMap T)
-  :=
-  match ls with
-  | hashmap.List.Cons k v tl =>
-    do
-    let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
-    hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
-  | hashmap.List.Nil => Result.ok ntable
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
-   Source: 'tests/src/hashmap.rs', lines 183:4-183:72 -/
-def hashmap.HashMap.move_elements_from_list
-  (T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) :
-  Result (hashmap.HashMap T)
-  :=
-  hashmap.HashMap.move_elements_from_list_loop T ntable ls
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 171:4-180:5 -/
-divergent def hashmap.HashMap.move_elements_loop
-  (T : Type) (ntable : hashmap.HashMap T)
-  (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
-  Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
-  :=
-  let i1 := alloc.vec.Vec.len (hashmap.List T) slots
-  if i < i1
-  then
-    do
-    let (l, index_mut_back) ←
-      alloc.vec.Vec.index_mut (hashmap.List T) Usize
-        (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) slots i
-    let (ls, l1) := core.mem.replace (hashmap.List T) l hashmap.List.Nil
-    let ntable1 ← hashmap.HashMap.move_elements_from_list T ntable ls
-    let i2 ← i + 1#usize
-    let slots1 ← index_mut_back l1
-    hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
-  else Result.ok (ntable, slots)
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
-   Source: 'tests/src/hashmap.rs', lines 171:4-171:95 -/
-def hashmap.HashMap.move_elements
-  (T : Type) (ntable : hashmap.HashMap T)
-  (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
-  Result ((hashmap.HashMap T) × (alloc.vec.Vec (hashmap.List T)))
-  :=
-  hashmap.HashMap.move_elements_loop T ntable slots i
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
-   Source: 'tests/src/hashmap.rs', lines 140:4-140:28 -/
-def hashmap.HashMap.try_resize
-  (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
-  do
-  let max_usize ← Scalar.cast .Usize core_u32_max
-  let capacity := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let n1 ← max_usize / 2#usize
-  let (i, i1) := self.max_load_factor
-  let i2 ← n1 / i
-  if capacity <= i2
-  then
-    do
-    let i3 ← capacity * 2#usize
-    let ntable ← hashmap.HashMap.new_with_capacity T i3 i i1
-    let p ← hashmap.HashMap.move_elements T ntable self.slots 0#usize
-    let (ntable1, _) := p
-    Result.ok
-      {
-        ntable1
-          with
-          num_entries := self.num_entries, max_load_factor := (i, i1)
-      }
-  else Result.ok { self with max_load_factor := (i, i1) }
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]:
-   Source: 'tests/src/hashmap.rs', lines 129:4-129:48 -/
-def hashmap.HashMap.insert
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) :
-  Result (hashmap.HashMap T)
-  :=
-  do
-  let self1 ← hashmap.HashMap.insert_no_resize T self key value
-  let i ← hashmap.HashMap.len T self1
-  if i > self1.max_load
-  then hashmap.HashMap.try_resize T self1
-  else Result.ok self1
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 206:4-219:5 -/
-divergent def hashmap.HashMap.contains_key_in_list_loop
-  (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool :=
-  match ls with
-  | hashmap.List.Cons ckey _ tl =>
-    if ckey = key
-    then Result.ok true
-    else hashmap.HashMap.contains_key_in_list_loop T key tl
-  | hashmap.List.Nil => Result.ok false
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 206:4-206:68 -/
-def hashmap.HashMap.contains_key_in_list
-  (T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool :=
-  hashmap.HashMap.contains_key_in_list_loop T key ls
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]:
-   Source: 'tests/src/hashmap.rs', lines 199:4-199:49 -/
-def hashmap.HashMap.contains_key
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool :=
-  do
-  let hash ← hashmap.hash_key key
-  let i := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let hash_mod ← hash % i
-  let l ←
-    alloc.vec.Vec.index (hashmap.List T) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
-      hash_mod
-  hashmap.HashMap.contains_key_in_list T key l
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 224:4-237:5 -/
-divergent def hashmap.HashMap.get_in_list_loop
-  (T : Type) (key : Usize) (ls : hashmap.List T) : Result T :=
-  match ls with
-  | hashmap.List.Cons ckey cvalue tl =>
-    if ckey = key
-    then Result.ok cvalue
-    else hashmap.HashMap.get_in_list_loop T key tl
-  | hashmap.List.Nil => Result.fail .panic
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 224:4-224:70 -/
-def hashmap.HashMap.get_in_list
-  (T : Type) (key : Usize) (ls : hashmap.List T) : Result T :=
-  hashmap.HashMap.get_in_list_loop T key ls
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]:
-   Source: 'tests/src/hashmap.rs', lines 239:4-239:55 -/
-def hashmap.HashMap.get
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T :=
-  do
-  let hash ← hashmap.hash_key key
-  let i := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let hash_mod ← hash % i
-  let l ←
-    alloc.vec.Vec.index (hashmap.List T) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
-      hash_mod
-  hashmap.HashMap.get_in_list T key l
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 245:4-254:5 -/
-divergent def hashmap.HashMap.get_mut_in_list_loop
-  (T : Type) (ls : hashmap.List T) (key : Usize) :
-  Result (T × (T → Result (hashmap.List T)))
-  :=
-  match ls with
-  | hashmap.List.Cons ckey cvalue tl =>
-    if ckey = key
-    then
-      let back := fun ret => Result.ok (hashmap.List.Cons ckey ret tl)
-      Result.ok (cvalue, back)
-    else
-      do
-      let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
-      let back1 :=
-        fun ret =>
-          do
-          let tl1 ← back ret
-          Result.ok (hashmap.List.Cons ckey cvalue tl1)
-      Result.ok (t, back1)
-  | hashmap.List.Nil => Result.fail .panic
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
-   Source: 'tests/src/hashmap.rs', lines 245:4-245:86 -/
-def hashmap.HashMap.get_mut_in_list
-  (T : Type) (ls : hashmap.List T) (key : Usize) :
-  Result (T × (T → Result (hashmap.List T)))
-  :=
-  hashmap.HashMap.get_mut_in_list_loop T ls key
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
-   Source: 'tests/src/hashmap.rs', lines 257:4-257:67 -/
-def hashmap.HashMap.get_mut
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) :
-  Result (T × (T → Result (hashmap.HashMap T)))
-  :=
-  do
-  let hash ← hashmap.hash_key key
-  let i := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let hash_mod ← hash % i
-  let (l, index_mut_back) ←
-    alloc.vec.Vec.index_mut (hashmap.List T) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
-      hash_mod
-  let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key
-  let back :=
-    fun ret =>
-      do
-      let l1 ← get_mut_in_list_back ret
-      let v ← index_mut_back l1
-      Result.ok { self with slots := v }
-  Result.ok (t, back)
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
-   Source: 'tests/src/hashmap.rs', lines 265:4-291:5 -/
-divergent def hashmap.HashMap.remove_from_list_loop
-  (T : Type) (key : Usize) (ls : hashmap.List T) :
-  Result ((Option T) × (hashmap.List T))
-  :=
-  match ls with
-  | hashmap.List.Cons ckey t tl =>
-    if ckey = key
-    then
-      let (mv_ls, _) :=
-        core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl)
-          hashmap.List.Nil
-      match mv_ls with
-      | hashmap.List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
-      | hashmap.List.Nil => Result.fail .panic
-    else
-      do
-      let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl
-      Result.ok (o, hashmap.List.Cons ckey t tl1)
-  | hashmap.List.Nil => Result.ok (none, hashmap.List.Nil)
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
-   Source: 'tests/src/hashmap.rs', lines 265:4-265:69 -/
-def hashmap.HashMap.remove_from_list
-  (T : Type) (key : Usize) (ls : hashmap.List T) :
-  Result ((Option T) × (hashmap.List T))
-  :=
-  hashmap.HashMap.remove_from_list_loop T key ls
-
-/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]:
-   Source: 'tests/src/hashmap.rs', lines 294:4-294:52 -/
-def hashmap.HashMap.remove
-  (T : Type) (self : hashmap.HashMap T) (key : Usize) :
-  Result ((Option T) × (hashmap.HashMap T))
-  :=
-  do
-  let hash ← hashmap.hash_key key
-  let i := alloc.vec.Vec.len (hashmap.List T) self.slots
-  let hash_mod ← hash % i
-  let (l, index_mut_back) ←
-    alloc.vec.Vec.index_mut (hashmap.List T) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
-      hash_mod
-  let (x, l1) ← hashmap.HashMap.remove_from_list T key l
-  match x with
-  | none =>
-    do
-    let v ← index_mut_back l1
-    Result.ok (none, { self with slots := v })
-  | some x1 =>
-    do
-    let i1 ← self.num_entries - 1#usize
-    let v ← index_mut_back l1
-    Result.ok (some x1, { self with num_entries := i1, slots := v })
-
-/- [hashmap_main::hashmap::test1]:
-   Source: 'tests/src/hashmap.rs', lines 315:0-315:10 -/
-def hashmap.test1 : Result Unit :=
-  do
-  let hm ← hashmap.HashMap.new U64
-  let hm1 ← hashmap.HashMap.insert U64 hm 0#usize 42#u64
-  let hm2 ← hashmap.HashMap.insert U64 hm1 128#usize 18#u64
-  let hm3 ← hashmap.HashMap.insert U64 hm2 1024#usize 138#u64
-  let hm4 ← hashmap.HashMap.insert U64 hm3 1056#usize 256#u64
-  let i ← hashmap.HashMap.get U64 hm4 128#usize
-  if ¬ (i = 18#u64)
-  then Result.fail .panic
-  else
-    do
-    let (_, get_mut_back) ← hashmap.HashMap.get_mut U64 hm4 1024#usize
-    let hm5 ← get_mut_back 56#u64
-    let i1 ← hashmap.HashMap.get U64 hm5 1024#usize
-    if ¬ (i1 = 56#u64)
-    then Result.fail .panic
-    else
-      do
-      let (x, hm6) ← hashmap.HashMap.remove U64 hm5 1024#usize
-      match x with
-      | none => Result.fail .panic
-      | some x1 =>
-        if ¬ (x1 = 56#u64)
-        then Result.fail .panic
-        else
-          do
-          let i2 ← hashmap.HashMap.get U64 hm6 0#usize
-          if ¬ (i2 = 42#u64)
-          then Result.fail .panic
-          else
-            do
-            let i3 ← hashmap.HashMap.get U64 hm6 128#usize
-            if ¬ (i3 = 18#u64)
-            then Result.fail .panic
-            else
-              do
-              let i4 ← hashmap.HashMap.get U64 hm6 1056#usize
-              if ¬ (i4 = 256#u64)
-              then Result.fail .panic
-              else Result.ok ()
-
-/- [hashmap_main::insert_on_disk]:
-   Source: 'tests/src/hashmap_main.rs', lines 7:0-7:43 -/
-def insert_on_disk
-  (key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
-  do
-  let (st1, hm) ← hashmap_utils.deserialize st
-  let hm1 ← hashmap.HashMap.insert U64 hm key value
-  hashmap_utils.serialize hm1 st1
-
-/- [hashmap_main::main]:
-   Source: 'tests/src/hashmap_main.rs', lines 16:0-16:13 -/
-def main : Result Unit :=
-  Result.ok ()
-
-end hashmap_main
diff --git a/tests/lean/HashmapMain/FunsExternal.lean b/tests/lean/HashmapMain/FunsExternal.lean
deleted file mode 100644
index b394b32b..00000000
--- a/tests/lean/HashmapMain/FunsExternal.lean
+++ /dev/null
@@ -1,17 +0,0 @@
--- [hashmap_main]: templates for the external functions.
-import Base
-import HashmapMain.Types
-open Primitives
-open hashmap_main
-
--- TODO: fill those bodies
-
-/- [hashmap_main::hashmap_utils::deserialize] -/
-def hashmap_utils.deserialize
-  : State → Result (State × (hashmap.HashMap U64)) :=
-  fun _ => .fail .panic
-
-/- [hashmap_main::hashmap_utils::serialize] -/
-def hashmap_utils.serialize
-  : hashmap.HashMap U64 → State → Result (State × Unit) :=
-  fun _ _ => .fail .panic
diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean
deleted file mode 100644
index c9c41608..00000000
--- a/tests/lean/HashmapMain/FunsExternal_Template.lean
+++ /dev/null
@@ -1,18 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [hashmap_main]: external functions.
--- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
-import Base
-import HashmapMain.Types
-open Primitives
-open hashmap_main
-
-/- [hashmap_main::hashmap_utils::deserialize]:
-   Source: 'tests/src/hashmap_utils.rs', lines 10:0-10:43 -/
-axiom hashmap_utils.deserialize
-  : State → Result (State × (hashmap.HashMap U64))
-
-/- [hashmap_main::hashmap_utils::serialize]:
-   Source: 'tests/src/hashmap_utils.rs', lines 5:0-5:42 -/
-axiom hashmap_utils.serialize
-  : hashmap.HashMap U64 → State → Result (State × Unit)
-
diff --git a/tests/lean/HashmapMain/Opaque.lean b/tests/lean/HashmapMain/Opaque.lean
deleted file mode 100644
index a410b253..00000000
--- a/tests/lean/HashmapMain/Opaque.lean
+++ /dev/null
@@ -1,18 +0,0 @@
--- [hashmap_main]: opaque function definitions
-import Base
-import HashmapMain.Types
-open Primitives
-
-namespace hashmap_main
-
-structure OpaqueDefs where
-  
-  /- [hashmap_main::hashmap_utils::deserialize] -/
-  hashmap_utils.deserialize_fwd
-    : 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)
-  
-end hashmap_main
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
deleted file mode 100644
index 076fb9ea..00000000
--- a/tests/lean/HashmapMain/Types.lean
+++ /dev/null
@@ -1,23 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [hashmap_main]: type definitions
-import Base
-import HashmapMain.TypesExternal
-open Primitives
-
-namespace hashmap_main
-
-/- [hashmap_main::hashmap::List]
-   Source: 'tests/src/hashmap.rs', lines 19:0-19:16 -/
-inductive hashmap.List (T : Type) :=
-| Cons : Usize → T → hashmap.List T → hashmap.List T
-| Nil : hashmap.List T
-
-/- [hashmap_main::hashmap::HashMap]
-   Source: 'tests/src/hashmap.rs', lines 35:0-35:21 -/
-structure hashmap.HashMap (T : Type) where
-  num_entries : Usize
-  max_load_factor : (Usize × Usize)
-  max_load : Usize
-  slots : alloc.vec.Vec (hashmap.List T)
-
-end hashmap_main
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
new file mode 100644
index 00000000..9eb8e22c
--- /dev/null
+++ b/tests/lean/InfiniteLoop.lean
@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [infinite_loop]
+import Base
+open Primitives
+
+namespace infinite_loop
+
+/- [infinite_loop::bar]:
+   Source: 'tests/src/infinite-loop.rs', lines 4:0-4:8 -/
+def bar : Result Unit :=
+  Result.ok ()
+
+/- [infinite_loop::foo]: loop 0:
+   Source: 'tests/src/infinite-loop.rs', lines 6:0-10:1 -/
+divergent def foo_loop : Result Unit :=
+  do
+  let _ ← bar
+  foo_loop
+
+/- [infinite_loop::foo]:
+   Source: 'tests/src/infinite-loop.rs', lines 6:0-6:8 -/
+def foo : Result Unit :=
+  foo_loop
+
+end infinite_loop
diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean
new file mode 100644
index 00000000..4eb23934
--- /dev/null
+++ b/tests/lean/Issue194RecursiveStructProjector.lean
@@ -0,0 +1,35 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [issue_194_recursive_struct_projector]
+import Base
+open Primitives
+
+namespace issue_194_recursive_struct_projector
+
+/- [issue_194_recursive_struct_projector::AVLNode]
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 -/
+inductive AVLNode (T : Type) :=
+| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T
+
+@[simp, reducible]
+def AVLNode.value {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk x1 _ _ => x1
+
+@[simp, reducible]
+def AVLNode.left {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk _ x1 _ => x1
+
+@[simp, reducible]
+def AVLNode.right {T : Type} (x : AVLNode T) :=
+  match x with | AVLNode.mk _ _ x1 => x1
+
+/- [issue_194_recursive_struct_projector::get_val]:
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 -/
+def get_val (T : Type) (x : AVLNode T) : Result T :=
+  Result.ok x.value
+
+/- [issue_194_recursive_struct_projector::get_left]:
+   Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 -/
+def get_left (T : Type) (x : AVLNode T) : Result (Option (AVLNode T)) :=
+  Result.ok x.left
+
+end issue_194_recursive_struct_projector
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index d5bda6ab..199605d5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -6,7 +6,7 @@ open Primitives
 namespace loops
 
 /- [loops::sum]: loop 0:
-   Source: 'tests/src/loops.rs', lines 4:0-14:1 -/
+   Source: 'tests/src/loops.rs', lines 8:0-18:1 -/
 divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then do
@@ -16,12 +16,12 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   else s * 2#u32
 
 /- [loops::sum]:
-   Source: 'tests/src/loops.rs', lines 4:0-4:27 -/
+   Source: 'tests/src/loops.rs', lines 8:0-8:27 -/
 def sum (max : U32) : Result U32 :=
   sum_loop max 0#u32 0#u32
 
 /- [loops::sum_with_mut_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 19:0-31:1 -/
+   Source: 'tests/src/loops.rs', lines 23:0-35:1 -/
 divergent def sum_with_mut_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -33,12 +33,12 @@ divergent def sum_with_mut_borrows_loop
   else s * 2#u32
 
 /- [loops::sum_with_mut_borrows]:
-   Source: 'tests/src/loops.rs', lines 19:0-19:44 -/
+   Source: 'tests/src/loops.rs', lines 23:0-23:44 -/
 def sum_with_mut_borrows (max : U32) : Result U32 :=
   sum_with_mut_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_with_shared_borrows]: loop 0:
-   Source: 'tests/src/loops.rs', lines 34:0-48:1 -/
+   Source: 'tests/src/loops.rs', lines 38:0-52:1 -/
 divergent def sum_with_shared_borrows_loop
   (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
@@ -50,12 +50,12 @@ divergent def sum_with_shared_borrows_loop
   else s * 2#u32
 
 /- [loops::sum_with_shared_borrows]:
-   Source: 'tests/src/loops.rs', lines 34:0-34:47 -/
+   Source: 'tests/src/loops.rs', lines 38:0-38:47 -/
 def sum_with_shared_borrows (max : U32) : Result U32 :=
   sum_with_shared_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_array]: loop 0:
-   Source: 'tests/src/loops.rs', lines 50:0-58:1 -/
+   Source: 'tests/src/loops.rs', lines 54:0-62:1 -/
 divergent def sum_array_loop
   (N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
   if i < N
@@ -68,12 +68,12 @@ divergent def sum_array_loop
   else Result.ok s
 
 /- [loops::sum_array]:
-   Source: 'tests/src/loops.rs', lines 50:0-50:52 -/
+   Source: 'tests/src/loops.rs', lines 54:0-54:52 -/
 def sum_array (N : Usize) (a : Array U32 N) : Result U32 :=
   sum_array_loop N a 0#usize 0#u32
 
 /- [loops::clear]: loop 0:
-   Source: 'tests/src/loops.rs', lines 62:0-68:1 -/
+   Source: 'tests/src/loops.rs', lines 66:0-72:1 -/
 divergent def clear_loop
   (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
   let i1 := alloc.vec.Vec.len U32 v
@@ -89,18 +89,18 @@ divergent def clear_loop
   else Result.ok v
 
 /- [loops::clear]:
-   Source: 'tests/src/loops.rs', lines 62:0-62:30 -/
+   Source: 'tests/src/loops.rs', lines 66:0-66:30 -/
 def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
   clear_loop v 0#usize
 
 /- [loops::List]
-   Source: 'tests/src/loops.rs', lines 70:0-70:16 -/
+   Source: 'tests/src/loops.rs', lines 74:0-74:16 -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
 /- [loops::list_mem]: loop 0:
-   Source: 'tests/src/loops.rs', lines 76:0-85:1 -/
+   Source: 'tests/src/loops.rs', lines 80:0-89:1 -/
 divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
   match ls with
   | List.Cons y tl => if y = x
@@ -109,12 +109,12 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
   | List.Nil => Result.ok false
 
 /- [loops::list_mem]:
-   Source: 'tests/src/loops.rs', lines 76:0-76:52 -/
+   Source: 'tests/src/loops.rs', lines 80:0-80:52 -/
 def list_mem (x : U32) (ls : List U32) : Result Bool :=
   list_mem_loop x ls
 
 /- [loops::list_nth_mut_loop]: loop 0:
-   Source: 'tests/src/loops.rs', lines 88:0-98:1 -/
+   Source: 'tests/src/loops.rs', lines 92:0-102:1 -/
 divergent def list_nth_mut_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match ls with
@@ -135,13 +135,13 @@ divergent def list_nth_mut_loop_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop]:
-   Source: 'tests/src/loops.rs', lines 88:0-88:71 -/
+   Source: 'tests/src/loops.rs', lines 92:0-92:71 -/
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   list_nth_mut_loop_loop T ls i
 
 /- [loops::list_nth_shared_loop]: loop 0:
-   Source: 'tests/src/loops.rs', lines 101:0-111:1 -/
+   Source: 'tests/src/loops.rs', lines 105:0-115:1 -/
 divergent def list_nth_shared_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
@@ -154,12 +154,12 @@ divergent def list_nth_shared_loop_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop]:
-   Source: 'tests/src/loops.rs', lines 101:0-101:66 -/
+   Source: 'tests/src/loops.rs', lines 105:0-105:66 -/
 def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
   list_nth_shared_loop_loop T ls i
 
 /- [loops::get_elem_mut]: loop 0:
-   Source: 'tests/src/loops.rs', lines 113:0-127:1 -/
+   Source: 'tests/src/loops.rs', lines 117:0-131:1 -/
 divergent def get_elem_mut_loop
   (x : Usize) (ls : List Usize) :
   Result (Usize × (Usize → Result (List Usize)))
@@ -181,7 +181,7 @@ divergent def get_elem_mut_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_mut]:
-   Source: 'tests/src/loops.rs', lines 113:0-113:73 -/
+   Source: 'tests/src/loops.rs', lines 117:0-117:73 -/
 def get_elem_mut
   (slots : alloc.vec.Vec (List Usize)) (x : Usize) :
   Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
@@ -197,7 +197,7 @@ def get_elem_mut
   Result.ok (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
-   Source: 'tests/src/loops.rs', lines 129:0-143:1 -/
+   Source: 'tests/src/loops.rs', lines 133:0-147:1 -/
 divergent def get_elem_shared_loop
   (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
@@ -207,7 +207,7 @@ divergent def get_elem_shared_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_shared]:
-   Source: 'tests/src/loops.rs', lines 129:0-129:68 -/
+   Source: 'tests/src/loops.rs', lines 133:0-133:68 -/
 def get_elem_shared
   (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
   do
@@ -217,7 +217,7 @@ def get_elem_shared
   get_elem_shared_loop x ls
 
 /- [loops::id_mut]:
-   Source: 'tests/src/loops.rs', lines 145:0-145:50 -/
+   Source: 'tests/src/loops.rs', lines 149:0-149:50 -/
 def id_mut
   (T : Type) (ls : List T) :
   Result ((List T) × (List T → Result (List T)))
@@ -225,12 +225,12 @@ def id_mut
   Result.ok (ls, Result.ok)
 
 /- [loops::id_shared]:
-   Source: 'tests/src/loops.rs', lines 149:0-149:45 -/
+   Source: 'tests/src/loops.rs', lines 153:0-153:45 -/
 def id_shared (T : Type) (ls : List T) : Result (List T) :=
   Result.ok ls
 
 /- [loops::list_nth_mut_loop_with_id]: loop 0:
-   Source: 'tests/src/loops.rs', lines 154:0-165:1 -/
+   Source: 'tests/src/loops.rs', lines 158:0-169:1 -/
 divergent def list_nth_mut_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result (T × (T → Result (List T))) :=
   match ls with
@@ -251,7 +251,7 @@ divergent def list_nth_mut_loop_with_id_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_with_id]:
-   Source: 'tests/src/loops.rs', lines 154:0-154:75 -/
+   Source: 'tests/src/loops.rs', lines 158:0-158:75 -/
 def list_nth_mut_loop_with_id
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   do
@@ -263,7 +263,7 @@ def list_nth_mut_loop_with_id
   Result.ok (t, back1)
 
 /- [loops::list_nth_shared_loop_with_id]: loop 0:
-   Source: 'tests/src/loops.rs', lines 168:0-179:1 -/
+   Source: 'tests/src/loops.rs', lines 172:0-183:1 -/
 divergent def list_nth_shared_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
@@ -276,7 +276,7 @@ divergent def list_nth_shared_loop_with_id_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_with_id]:
-   Source: 'tests/src/loops.rs', lines 168:0-168:70 -/
+   Source: 'tests/src/loops.rs', lines 172:0-172:70 -/
 def list_nth_shared_loop_with_id
   (T : Type) (ls : List T) (i : U32) : Result T :=
   do
@@ -284,7 +284,7 @@ def list_nth_shared_loop_with_id
   list_nth_shared_loop_with_id_loop T i ls1
 
 /- [loops::list_nth_mut_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 184:0-205:1 -/
+   Source: 'tests/src/loops.rs', lines 188:0-209:1 -/
 divergent def list_nth_mut_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -315,7 +315,7 @@ divergent def list_nth_mut_loop_pair_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair]:
-   Source: 'tests/src/loops.rs', lines 184:0-188:27 -/
+   Source: 'tests/src/loops.rs', lines 188:0-192:27 -/
 def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -323,7 +323,7 @@ def list_nth_mut_loop_pair
   list_nth_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 208:0-229:1 -/
+   Source: 'tests/src/loops.rs', lines 212:0-233:1 -/
 divergent def list_nth_shared_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
@@ -339,13 +339,13 @@ divergent def list_nth_shared_loop_pair_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_pair]:
-   Source: 'tests/src/loops.rs', lines 208:0-212:19 -/
+   Source: 'tests/src/loops.rs', lines 212:0-216:19 -/
 def list_nth_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 233:0-248:1 -/
+   Source: 'tests/src/loops.rs', lines 237:0-252:1 -/
 divergent def list_nth_mut_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -375,7 +375,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_pair_merge]:
-   Source: 'tests/src/loops.rs', lines 233:0-237:27 -/
+   Source: 'tests/src/loops.rs', lines 237:0-241:27 -/
 def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -383,7 +383,7 @@ def list_nth_mut_loop_pair_merge
   list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 251:0-266:1 -/
+   Source: 'tests/src/loops.rs', lines 255:0-270:1 -/
 divergent def list_nth_shared_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   match ls0 with
@@ -400,13 +400,13 @@ divergent def list_nth_shared_loop_pair_merge_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_loop_pair_merge]:
-   Source: 'tests/src/loops.rs', lines 251:0-255:19 -/
+   Source: 'tests/src/loops.rs', lines 255:0-259:19 -/
 def list_nth_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 269:0-284:1 -/
+   Source: 'tests/src/loops.rs', lines 273:0-288:1 -/
 divergent def list_nth_mut_shared_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -432,7 +432,7 @@ divergent def list_nth_mut_shared_loop_pair_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair]:
-   Source: 'tests/src/loops.rs', lines 269:0-273:23 -/
+   Source: 'tests/src/loops.rs', lines 273:0-277:23 -/
 def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -440,7 +440,7 @@ def list_nth_mut_shared_loop_pair
   list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 288:0-303:1 -/
+   Source: 'tests/src/loops.rs', lines 292:0-307:1 -/
 divergent def list_nth_mut_shared_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -466,7 +466,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]:
-   Source: 'tests/src/loops.rs', lines 288:0-292:23 -/
+   Source: 'tests/src/loops.rs', lines 292:0-296:23 -/
 def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -474,7 +474,7 @@ def list_nth_mut_shared_loop_pair_merge
   list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair]: loop 0:
-   Source: 'tests/src/loops.rs', lines 307:0-322:1 -/
+   Source: 'tests/src/loops.rs', lines 311:0-326:1 -/
 divergent def list_nth_shared_mut_loop_pair_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -500,7 +500,7 @@ divergent def list_nth_shared_mut_loop_pair_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair]:
-   Source: 'tests/src/loops.rs', lines 307:0-311:23 -/
+   Source: 'tests/src/loops.rs', lines 311:0-315:23 -/
 def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -508,7 +508,7 @@ def list_nth_shared_mut_loop_pair
   list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
-   Source: 'tests/src/loops.rs', lines 326:0-341:1 -/
+   Source: 'tests/src/loops.rs', lines 330:0-345:1 -/
 divergent def list_nth_shared_mut_loop_pair_merge_loop
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -534,7 +534,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]:
-   Source: 'tests/src/loops.rs', lines 326:0-330:23 -/
+   Source: 'tests/src/loops.rs', lines 330:0-334:23 -/
 def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -542,7 +542,7 @@ def list_nth_shared_mut_loop_pair_merge
   list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
 
 /- [loops::ignore_input_mut_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 345:0-349:1 -/
+   Source: 'tests/src/loops.rs', lines 349:0-353:1 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
@@ -551,14 +551,14 @@ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   else Result.ok ()
 
 /- [loops::ignore_input_mut_borrow]:
-   Source: 'tests/src/loops.rs', lines 345:0-345:56 -/
+   Source: 'tests/src/loops.rs', lines 349:0-349:56 -/
 def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
   do
   let _ ← ignore_input_mut_borrow_loop i
   Result.ok _a
 
 /- [loops::incr_ignore_input_mut_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 353:0-358:1 -/
+   Source: 'tests/src/loops.rs', lines 357:0-362:1 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
@@ -567,7 +567,7 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   else Result.ok ()
 
 /- [loops::incr_ignore_input_mut_borrow]:
-   Source: 'tests/src/loops.rs', lines 353:0-353:60 -/
+   Source: 'tests/src/loops.rs', lines 357:0-357:60 -/
 def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
   do
   let a1 ← a + 1#u32
@@ -575,7 +575,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
   Result.ok a1
 
 /- [loops::ignore_input_shared_borrow]: loop 0:
-   Source: 'tests/src/loops.rs', lines 362:0-366:1 -/
+   Source: 'tests/src/loops.rs', lines 366:0-370:1 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   if i > 0#u32
   then do
@@ -584,7 +584,7 @@ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   else Result.ok ()
 
 /- [loops::ignore_input_shared_borrow]:
-   Source: 'tests/src/loops.rs', lines 362:0-362:59 -/
+   Source: 'tests/src/loops.rs', lines 366:0-366:59 -/
 def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
   do
   let _ ← ignore_input_shared_borrow_loop i
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
new file mode 100644
index 00000000..3e3a558b
--- /dev/null
+++ b/tests/lean/Matches.lean
@@ -0,0 +1,16 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [matches]
+import Base
+open Primitives
+
+namespace matches
+
+/- [matches::match_u32]:
+   Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
+def match_u32 (x : U32) : Result U32 :=
+  match x with
+  | 0#u32 => Result.ok 0#u32
+  | 1#u32 => Result.ok 1#u32
+  | _ => Result.ok 2#u32
+
+end matches
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 0f11092d..aa782009 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -6,60 +6,60 @@ open Primitives
 namespace no_nested_borrows
 
 /- [no_nested_borrows::Pair]
-   Source: 'tests/src/no_nested_borrows.rs', lines 4:0-4:23 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 7:0-7:23 -/
 structure Pair (T1 T2 : Type) where
   x : T1
   y : T2
 
 /- [no_nested_borrows::List]
-   Source: 'tests/src/no_nested_borrows.rs', lines 9:0-9:16 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 12:0-12:16 -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
 /- [no_nested_borrows::One]
-   Source: 'tests/src/no_nested_borrows.rs', lines 20:0-20:16 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 23:0-23:16 -/
 inductive One (T1 : Type) :=
 | One : T1 → One T1
 
 /- [no_nested_borrows::EmptyEnum]
-   Source: 'tests/src/no_nested_borrows.rs', lines 26:0-26:18 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 29:0-29:18 -/
 inductive EmptyEnum :=
 | Empty : EmptyEnum
 
 /- [no_nested_borrows::Enum]
-   Source: 'tests/src/no_nested_borrows.rs', lines 32:0-32:13 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 35:0-35:13 -/
 inductive Enum :=
 | Variant1 : Enum
 | Variant2 : Enum
 
 /- [no_nested_borrows::EmptyStruct]
-   Source: 'tests/src/no_nested_borrows.rs', lines 39:0-39:22 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 42:0-42:22 -/
 @[reducible] def EmptyStruct := Unit
 
 /- [no_nested_borrows::Sum]
-   Source: 'tests/src/no_nested_borrows.rs', lines 41:0-41:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 44:0-44:20 -/
 inductive Sum (T1 T2 : Type) :=
 | Left : T1 → Sum T1 T2
 | Right : T2 → Sum T1 T2
 
 /- [no_nested_borrows::cast_u32_to_i32]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 46:0-46:37 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 49:0-49:37 -/
 def cast_u32_to_i32 (x : U32) : Result I32 :=
   Scalar.cast .I32 x
 
 /- [no_nested_borrows::cast_bool_to_i32]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 50:0-50:39 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 53:0-53:39 -/
 def cast_bool_to_i32 (x : Bool) : Result I32 :=
   Scalar.cast_bool .I32 x
 
 /- [no_nested_borrows::cast_bool_to_bool]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 55:0-55:41 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 58:0-58:41 -/
 def cast_bool_to_bool (x : Bool) : Result Bool :=
   Result.ok x
 
 /- [no_nested_borrows::test2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 60:0-60:14 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/
 def test2 : Result Unit :=
   do
   let _ ← 23#u32 + 44#u32
@@ -69,14 +69,14 @@ def test2 : Result Unit :=
 #assert (test2 == Result.ok ())
 
 /- [no_nested_borrows::get_max]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 72:0-72:37 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 75:0-75:37 -/
 def get_max (x : U32) (y : U32) : Result U32 :=
   if x >= y
   then Result.ok x
   else Result.ok y
 
 /- [no_nested_borrows::test3]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 80:0-80:14 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/
 def test3 : Result Unit :=
   do
   let x ← get_max 4#u32 3#u32
@@ -90,7 +90,7 @@ def test3 : Result Unit :=
 #assert (test3 == Result.ok ())
 
 /- [no_nested_borrows::test_neg1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 87:0-87:18 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/
 def test_neg1 : Result Unit :=
   do
   let y ← -. 3#i32
@@ -102,7 +102,7 @@ def test_neg1 : Result Unit :=
 #assert (test_neg1 == Result.ok ())
 
 /- [no_nested_borrows::refs_test1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 94:0-94:19 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/
 def refs_test1 : Result Unit :=
   if ¬ (1#i32 = 1#i32)
   then Result.fail .panic
@@ -112,7 +112,7 @@ def refs_test1 : Result Unit :=
 #assert (refs_test1 == Result.ok ())
 
 /- [no_nested_borrows::refs_test2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 105:0-105:19 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/
 def refs_test2 : Result Unit :=
   if ¬ (2#i32 = 2#i32)
   then Result.fail .panic
@@ -130,7 +130,7 @@ def refs_test2 : Result Unit :=
 #assert (refs_test2 == Result.ok ())
 
 /- [no_nested_borrows::test_list1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 121:0-121:19 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 124:0-124:19 -/
 def test_list1 : Result Unit :=
   Result.ok ()
 
@@ -138,7 +138,7 @@ def test_list1 : Result Unit :=
 #assert (test_list1 == Result.ok ())
 
 /- [no_nested_borrows::test_box1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 126:0-126:18 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 129:0-129:18 -/
 def test_box1 : Result Unit :=
   do
   let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32
@@ -152,26 +152,26 @@ def test_box1 : Result Unit :=
 #assert (test_box1 == Result.ok ())
 
 /- [no_nested_borrows::copy_int]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 136:0-136:30 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 139:0-139:30 -/
 def copy_int (x : I32) : Result I32 :=
   Result.ok x
 
 /- [no_nested_borrows::test_unreachable]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 142:0-142:32 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 145:0-145:32 -/
 def test_unreachable (b : Bool) : Result Unit :=
   if b
   then Result.fail .panic
   else Result.ok ()
 
 /- [no_nested_borrows::test_panic]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 150:0-150:26 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 153:0-153:26 -/
 def test_panic (b : Bool) : Result Unit :=
   if b
   then Result.fail .panic
   else Result.ok ()
 
 /- [no_nested_borrows::test_copy_int]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 157:0-157:22 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/
 def test_copy_int : Result Unit :=
   do
   let y ← copy_int 0#i32
@@ -183,14 +183,14 @@ def test_copy_int : Result Unit :=
 #assert (test_copy_int == Result.ok ())
 
 /- [no_nested_borrows::is_cons]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 164:0-164:38 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 167:0-167:38 -/
 def is_cons (T : Type) (l : List T) : Result Bool :=
   match l with
   | List.Cons _ _ => Result.ok true
   | List.Nil => Result.ok false
 
 /- [no_nested_borrows::test_is_cons]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 171:0-171:21 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 -/
 def test_is_cons : Result Unit :=
   do
   let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
@@ -202,14 +202,14 @@ def test_is_cons : Result Unit :=
 #assert (test_is_cons == Result.ok ())
 
 /- [no_nested_borrows::split_list]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 177:0-177:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 180:0-180:48 -/
 def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
   match l with
   | List.Cons hd tl => Result.ok (hd, tl)
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::test_split_list]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 185:0-185:24 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 188:0-188:24 -/
 def test_split_list : Result Unit :=
   do
   let p ← split_list I32 (List.Cons 0#i32 List.Nil)
@@ -222,7 +222,7 @@ def test_split_list : Result Unit :=
 #assert (test_split_list == Result.ok ())
 
 /- [no_nested_borrows::choose]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 192:0-192:70 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 195:0-195:70 -/
 def choose
   (T : Type) (b : Bool) (x : T) (y : T) :
   Result (T × (T → Result (T × T)))
@@ -234,7 +234,7 @@ def choose
        Result.ok (y, back)
 
 /- [no_nested_borrows::choose_test]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 200:0-200:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 203:0-203:20 -/
 def choose_test : Result Unit :=
   do
   let (z, choose_back) ← choose I32 true 0#i32 0#i32
@@ -254,25 +254,25 @@ def choose_test : Result Unit :=
 #assert (choose_test == Result.ok ())
 
 /- [no_nested_borrows::test_char]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 212:0-212:26 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 215:0-215:26 -/
 def test_char : Result Char :=
   Result.ok 'a'
 
 /- [no_nested_borrows::panic_mut_borrow]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 217:0-217:36 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220:36 -/
 def panic_mut_borrow (i : U32) : Result U32 :=
   Result.fail .panic
 
 mutual
 
 /- [no_nested_borrows::Tree]
-   Source: 'tests/src/no_nested_borrows.rs', lines 222:0-222:16 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:16 -/
 inductive Tree (T : Type) :=
 | Leaf : T → Tree T
 | Node : T → NodeElem T → Tree T → Tree T
 
 /- [no_nested_borrows::NodeElem]
-   Source: 'tests/src/no_nested_borrows.rs', lines 227:0-227:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 230:0-230:20 -/
 inductive NodeElem (T : Type) :=
 | Cons : Tree T → NodeElem T → NodeElem T
 | Nil : NodeElem T
@@ -280,7 +280,7 @@ inductive NodeElem (T : Type) :=
 end
 
 /- [no_nested_borrows::list_length]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 262:0-262:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:48 -/
 divergent def list_length (T : Type) (l : List T) : Result U32 :=
   match l with
   | List.Cons _ l1 => do
@@ -289,7 +289,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
   | List.Nil => Result.ok 0#u32
 
 /- [no_nested_borrows::list_nth_shared]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 270:0-270:62 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/
 divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
@@ -301,7 +301,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_nth_mut]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 286:0-286:67 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 289:0-289:67 -/
 divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
@@ -323,7 +323,7 @@ divergent def list_nth_mut
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_rev_aux]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 302:0-302:63 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 305:0-305:63 -/
 divergent def list_rev_aux
   (T : Type) (li : List T) (lo : List T) : Result (List T) :=
   match li with
@@ -331,13 +331,13 @@ divergent def list_rev_aux
   | List.Nil => Result.ok lo
 
 /- [no_nested_borrows::list_rev]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 316:0-316:42 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:42 -/
 def list_rev (T : Type) (l : List T) : Result (List T) :=
   let (li, _) := core.mem.replace (List T) l List.Nil
   list_rev_aux T li List.Nil
 
 /- [no_nested_borrows::test_list_functions]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 321:0-321:28 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/
 def test_list_functions : Result Unit :=
   do
   let l := List.Cons 2#i32 List.Nil
@@ -384,7 +384,7 @@ def test_list_functions : Result Unit :=
 #assert (test_list_functions == Result.ok ())
 
 /- [no_nested_borrows::id_mut_pair1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 337:0-337:89 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:89 -/
 def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -392,7 +392,7 @@ def id_mut_pair1
   Result.ok ((x, y), Result.ok)
 
 /- [no_nested_borrows::id_mut_pair2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 341:0-341:88 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:88 -/
 def id_mut_pair2
   (T1 T2 : Type) (p : (T1 × T2)) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -401,7 +401,7 @@ def id_mut_pair2
   Result.ok ((t, t1), Result.ok)
 
 /- [no_nested_borrows::id_mut_pair3]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 345:0-345:93 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 348:0-348:93 -/
 def id_mut_pair3
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -409,7 +409,7 @@ def id_mut_pair3
   Result.ok ((x, y), Result.ok, Result.ok)
 
 /- [no_nested_borrows::id_mut_pair4]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 349:0-349:92 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 352:0-352:92 -/
 def id_mut_pair4
   (T1 T2 : Type) (p : (T1 × T2)) :
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -418,37 +418,37 @@ def id_mut_pair4
   Result.ok ((t, t1), Result.ok, Result.ok)
 
 /- [no_nested_borrows::StructWithTuple]
-   Source: 'tests/src/no_nested_borrows.rs', lines 356:0-356:34 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:34 -/
 structure StructWithTuple (T1 T2 : Type) where
   p : (T1 × T2)
 
 /- [no_nested_borrows::new_tuple1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 360:0-360:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
   Result.ok { p := (1#u32, 2#u32) }
 
 /- [no_nested_borrows::new_tuple2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 364:0-364:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
   Result.ok { p := (1#i16, 2#i16) }
 
 /- [no_nested_borrows::new_tuple3]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 368:0-368:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
   Result.ok { p := (1#u64, 2#i64) }
 
 /- [no_nested_borrows::StructWithPair]
-   Source: 'tests/src/no_nested_borrows.rs', lines 373:0-373:33 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/
 structure StructWithPair (T1 T2 : Type) where
   p : Pair T1 T2
 
 /- [no_nested_borrows::new_pair1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 377:0-377:46 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
   Result.ok { p := { x := 1#u32, y := 2#u32 } }
 
 /- [no_nested_borrows::test_constants]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 385:0-385:23 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/
 def test_constants : Result Unit :=
   do
   let swt ← new_tuple1
@@ -478,7 +478,7 @@ def test_constants : Result Unit :=
 #assert (test_constants == Result.ok ())
 
 /- [no_nested_borrows::test_weird_borrows1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 394:0-394:28 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 397:0-397:28 -/
 def test_weird_borrows1 : Result Unit :=
   Result.ok ()
 
@@ -486,7 +486,7 @@ def test_weird_borrows1 : Result Unit :=
 #assert (test_weird_borrows1 == Result.ok ())
 
 /- [no_nested_borrows::test_mem_replace]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 404:0-404:37 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/
 def test_mem_replace (px : U32) : Result U32 :=
   let (y, _) := core.mem.replace U32 px 1#u32
   if ¬ (y = 0#u32)
@@ -494,71 +494,71 @@ def test_mem_replace (px : U32) : Result U32 :=
   else Result.ok 2#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 411:0-411:47 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/
 def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
   if b
   then Result.ok 0#u32
   else Result.ok 1#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 424:0-424:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/
 def test_shared_borrow_bool2 : Result U32 :=
   Result.ok 0#u32
 
 /- [no_nested_borrows::test_shared_borrow_enum1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 439:0-439:52 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/
 def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
   match l with
   | List.Cons _ _ => Result.ok 1#u32
   | List.Nil => Result.ok 0#u32
 
 /- [no_nested_borrows::test_shared_borrow_enum2]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 451:0-451:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/
 def test_shared_borrow_enum2 : Result U32 :=
   Result.ok 0#u32
 
 /- [no_nested_borrows::incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 462:0-462:24 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
 /- [no_nested_borrows::call_incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 466:0-466:35 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/
 def call_incr (x : U32) : Result U32 :=
   incr x
 
 /- [no_nested_borrows::read_then_incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 471:0-471:41 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/
 def read_then_incr (x : U32) : Result (U32 × U32) :=
   do
   let x1 ← x + 1#u32
   Result.ok (x, x1)
 
 /- [no_nested_borrows::Tuple]
-   Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477:24 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 -/
 def Tuple (T1 T2 : Type) := T1 × T2
 
 /- [no_nested_borrows::use_tuple_struct]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 479:0-479:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 -/
 def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
   Result.ok (1#u32, x.#1)
 
 /- [no_nested_borrows::create_tuple_struct]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 483:0-483:61 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 -/
 def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
   Result.ok (x, y)
 
 /- [no_nested_borrows::IdType]
-   Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 -/
 @[reducible] def IdType (T : Type) := T
 
 /- [no_nested_borrows::use_id_type]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 -/
 def use_id_type (T : Type) (x : IdType T) : Result T :=
   Result.ok x
 
 /- [no_nested_borrows::create_id_type]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:43 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 -/
 def create_id_type (T : Type) (x : T) : Result (IdType T) :=
   Result.ok x
 
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index bede3dd9..dbd56f3e 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -6,12 +6,12 @@ open Primitives
 namespace paper
 
 /- [paper::ref_incr]:
-   Source: 'tests/src/paper.rs', lines 4:0-4:28 -/
+   Source: 'tests/src/paper.rs', lines 7:0-7:28 -/
 def ref_incr (x : I32) : Result I32 :=
   x + 1#i32
 
 /- [paper::test_incr]:
-   Source: 'tests/src/paper.rs', lines 8:0-8:18 -/
+   Source: 'tests/src/paper.rs', lines 11:0-11:18 -/
 def test_incr : Result Unit :=
   do
   let x ← ref_incr 0#i32
@@ -23,7 +23,7 @@ def test_incr : Result Unit :=
 #assert (test_incr == Result.ok ())
 
 /- [paper::choose]:
-   Source: 'tests/src/paper.rs', lines 15:0-15:70 -/
+   Source: 'tests/src/paper.rs', lines 18:0-18:70 -/
 def choose
   (T : Type) (b : Bool) (x : T) (y : T) :
   Result (T × (T → Result (T × T)))
@@ -35,7 +35,7 @@ def choose
        Result.ok (y, back)
 
 /- [paper::test_choose]:
-   Source: 'tests/src/paper.rs', lines 23:0-23:20 -/
+   Source: 'tests/src/paper.rs', lines 26:0-26:20 -/
 def test_choose : Result Unit :=
   do
   let (z, choose_back) ← choose I32 true 0#i32 0#i32
@@ -55,13 +55,13 @@ def test_choose : Result Unit :=
 #assert (test_choose == Result.ok ())
 
 /- [paper::List]
-   Source: 'tests/src/paper.rs', lines 35:0-35:16 -/
+   Source: 'tests/src/paper.rs', lines 38:0-38:16 -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
 /- [paper::list_nth_mut]:
-   Source: 'tests/src/paper.rs', lines 42:0-42:67 -/
+   Source: 'tests/src/paper.rs', lines 45:0-45:67 -/
 divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
@@ -83,7 +83,7 @@ divergent def list_nth_mut
   | List.Nil => Result.fail .panic
 
 /- [paper::sum]:
-   Source: 'tests/src/paper.rs', lines 57:0-57:32 -/
+   Source: 'tests/src/paper.rs', lines 60:0-60:32 -/
 divergent def sum (l : List I32) : Result I32 :=
   match l with
   | List.Cons x tl => do
@@ -92,7 +92,7 @@ divergent def sum (l : List I32) : Result I32 :=
   | List.Nil => Result.ok 0#i32
 
 /- [paper::test_nth]:
-   Source: 'tests/src/paper.rs', lines 68:0-68:17 -/
+   Source: 'tests/src/paper.rs', lines 71:0-71:17 -/
 def test_nth : Result Unit :=
   do
   let l := List.Cons 3#i32 List.Nil
@@ -109,7 +109,7 @@ def test_nth : Result Unit :=
 #assert (test_nth == Result.ok ())
 
 /- [paper::call_choose]:
-   Source: 'tests/src/paper.rs', lines 76:0-76:44 -/
+   Source: 'tests/src/paper.rs', lines 79:0-79:44 -/
 def call_choose (p : (U32 × U32)) : Result U32 :=
   do
   let (px, py) := p
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index d1ed10d2..ed279d58 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -6,13 +6,13 @@ open Primitives
 namespace polonius_list
 
 /- [polonius_list::List]
-   Source: 'tests/src/polonius_list.rs', lines 3:0-3:16 -/
+   Source: 'tests/src/polonius_list.rs', lines 6:0-6:16 -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
 /- [polonius_list::get_list_at_x]:
-   Source: 'tests/src/polonius_list.rs', lines 13:0-13:76 -/
+   Source: 'tests/src/polonius_list.rs', lines 16:0-16:76 -/
 divergent def get_list_at_x
   (ls : List U32) (x : U32) :
   Result ((List U32) × (List U32 → Result (List U32)))
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 32f84676..7cacb836 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -6,29 +6,29 @@ open Primitives
 namespace traits
 
 /- Trait declaration: [traits::BoolTrait]
-   Source: 'tests/src/traits.rs', lines 1:0-1:19 -/
+   Source: 'tests/src/traits.rs', lines 2:0-2:19 -/
 structure BoolTrait (Self : Type) where
   get_bool : Self → Result Bool
 
 /- [traits::{(traits::BoolTrait for bool)}::get_bool]:
-   Source: 'tests/src/traits.rs', lines 12:4-12:30 -/
+   Source: 'tests/src/traits.rs', lines 13:4-13:30 -/
 def BoolTraitBool.get_bool (self : Bool) : Result Bool :=
   Result.ok self
 
 /- Trait implementation: [traits::{(traits::BoolTrait for bool)}]
-   Source: 'tests/src/traits.rs', lines 11:0-11:23 -/
+   Source: 'tests/src/traits.rs', lines 12:0-12:23 -/
 def BoolTraitBool : BoolTrait Bool := {
   get_bool := BoolTraitBool.get_bool
 }
 
 /- [traits::BoolTrait::ret_true]:
-   Source: 'tests/src/traits.rs', lines 6:4-6:30 -/
+   Source: 'tests/src/traits.rs', lines 7:4-7:30 -/
 def BoolTrait.ret_true
   {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
   Result.ok true
 
 /- [traits::test_bool_trait_bool]:
-   Source: 'tests/src/traits.rs', lines 17:0-17:44 -/
+   Source: 'tests/src/traits.rs', lines 18:0-18:44 -/
 def test_bool_trait_bool (x : Bool) : Result Bool :=
   do
   let b ← BoolTraitBool.get_bool x
@@ -37,20 +37,20 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
   else Result.ok false
 
 /- [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
-   Source: 'tests/src/traits.rs', lines 23:4-23:30 -/
+   Source: 'tests/src/traits.rs', lines 24:4-24:30 -/
 def BoolTraitOption.get_bool (T : Type) (self : Option T) : Result Bool :=
   match self with
   | none => Result.ok false
   | some _ => Result.ok true
 
 /- Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
-   Source: 'tests/src/traits.rs', lines 22:0-22:31 -/
+   Source: 'tests/src/traits.rs', lines 23:0-23:31 -/
 def BoolTraitOption (T : Type) : BoolTrait (Option T) := {
   get_bool := BoolTraitOption.get_bool T
 }
 
 /- [traits::test_bool_trait_option]:
-   Source: 'tests/src/traits.rs', lines 31:0-31:54 -/
+   Source: 'tests/src/traits.rs', lines 32:0-32:54 -/
 def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
   do
   let b ← BoolTraitOption.get_bool T x
@@ -59,29 +59,29 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
   else Result.ok false
 
 /- [traits::test_bool_trait]:
-   Source: 'tests/src/traits.rs', lines 35:0-35:50 -/
+   Source: 'tests/src/traits.rs', lines 36:0-36:50 -/
 def test_bool_trait
   (T : Type) (BoolTraitInst : BoolTrait T) (x : T) : Result Bool :=
   BoolTraitInst.get_bool x
 
 /- Trait declaration: [traits::ToU64]
-   Source: 'tests/src/traits.rs', lines 39:0-39:15 -/
+   Source: 'tests/src/traits.rs', lines 40:0-40:15 -/
 structure ToU64 (Self : Type) where
   to_u64 : Self → Result U64
 
 /- [traits::{(traits::ToU64 for u64)#2}::to_u64]:
-   Source: 'tests/src/traits.rs', lines 44:4-44:26 -/
+   Source: 'tests/src/traits.rs', lines 45:4-45:26 -/
 def ToU64U64.to_u64 (self : U64) : Result U64 :=
   Result.ok self
 
 /- Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
-   Source: 'tests/src/traits.rs', lines 43:0-43:18 -/
+   Source: 'tests/src/traits.rs', lines 44:0-44:18 -/
 def ToU64U64 : ToU64 U64 := {
   to_u64 := ToU64U64.to_u64
 }
 
 /- [traits::{(traits::ToU64 for (A, A))#3}::to_u64]:
-   Source: 'tests/src/traits.rs', lines 50:4-50:26 -/
+   Source: 'tests/src/traits.rs', lines 51:4-51:26 -/
 def ToU64Pair.to_u64
   (A : Type) (ToU64Inst : ToU64 A) (self : (A × A)) : Result U64 :=
   do
@@ -91,78 +91,78 @@ def ToU64Pair.to_u64
   i + i1
 
 /- Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}]
-   Source: 'tests/src/traits.rs', lines 49:0-49:31 -/
+   Source: 'tests/src/traits.rs', lines 50:0-50:31 -/
 def ToU64Pair (A : Type) (ToU64Inst : ToU64 A) : ToU64 (A × A) := {
   to_u64 := ToU64Pair.to_u64 A ToU64Inst
 }
 
 /- [traits::f]:
-   Source: 'tests/src/traits.rs', lines 55:0-55:36 -/
+   Source: 'tests/src/traits.rs', lines 56:0-56:36 -/
 def f (T : Type) (ToU64Inst : ToU64 T) (x : (T × T)) : Result U64 :=
   ToU64Pair.to_u64 T ToU64Inst x
 
 /- [traits::g]:
-   Source: 'tests/src/traits.rs', lines 59:0-61:18 -/
+   Source: 'tests/src/traits.rs', lines 60:0-62:18 -/
 def g
   (T : Type) (ToU64PairInst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
   ToU64PairInst.to_u64 x
 
 /- [traits::h0]:
-   Source: 'tests/src/traits.rs', lines 66:0-66:24 -/
+   Source: 'tests/src/traits.rs', lines 67:0-67:24 -/
 def h0 (x : U64) : Result U64 :=
   ToU64U64.to_u64 x
 
 /- [traits::Wrapper]
-   Source: 'tests/src/traits.rs', lines 70:0-70:21 -/
+   Source: 'tests/src/traits.rs', lines 71:0-71:21 -/
 structure Wrapper (T : Type) where
   x : T
 
 /- [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}::to_u64]:
-   Source: 'tests/src/traits.rs', lines 75:4-75:26 -/
+   Source: 'tests/src/traits.rs', lines 76:4-76:26 -/
 def ToU64traitsWrapper.to_u64
   (T : Type) (ToU64Inst : ToU64 T) (self : Wrapper T) : Result U64 :=
   ToU64Inst.to_u64 self.x
 
 /- Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}]
-   Source: 'tests/src/traits.rs', lines 74:0-74:35 -/
+   Source: 'tests/src/traits.rs', lines 75:0-75:35 -/
 def ToU64traitsWrapper (T : Type) (ToU64Inst : ToU64 T) : ToU64 (Wrapper T)
   := {
   to_u64 := ToU64traitsWrapper.to_u64 T ToU64Inst
 }
 
 /- [traits::h1]:
-   Source: 'tests/src/traits.rs', lines 80:0-80:33 -/
+   Source: 'tests/src/traits.rs', lines 81:0-81:33 -/
 def h1 (x : Wrapper U64) : Result U64 :=
   ToU64traitsWrapper.to_u64 U64 ToU64U64 x
 
 /- [traits::h2]:
-   Source: 'tests/src/traits.rs', lines 84:0-84:41 -/
+   Source: 'tests/src/traits.rs', lines 85:0-85:41 -/
 def h2 (T : Type) (ToU64Inst : ToU64 T) (x : Wrapper T) : Result U64 :=
   ToU64traitsWrapper.to_u64 T ToU64Inst x
 
 /- Trait declaration: [traits::ToType]
-   Source: 'tests/src/traits.rs', lines 88:0-88:19 -/
+   Source: 'tests/src/traits.rs', lines 89:0-89:19 -/
 structure ToType (Self T : Type) where
   to_type : Self → Result T
 
 /- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
-   Source: 'tests/src/traits.rs', lines 93:4-93:28 -/
+   Source: 'tests/src/traits.rs', lines 94:4-94:28 -/
 def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
   Result.ok (self > 0#u64)
 
 /- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
-   Source: 'tests/src/traits.rs', lines 92:0-92:25 -/
+   Source: 'tests/src/traits.rs', lines 93:0-93:25 -/
 def ToTypeU64Bool : ToType U64 Bool := {
   to_type := ToTypeU64Bool.to_type
 }
 
 /- Trait declaration: [traits::OfType]
-   Source: 'tests/src/traits.rs', lines 98:0-98:16 -/
+   Source: 'tests/src/traits.rs', lines 99:0-99:16 -/
 structure OfType (Self : Type) where
   of_type : forall (T : Type) (ToTypeInst : ToType T Self), T → Result Self
 
 /- [traits::h3]:
-   Source: 'tests/src/traits.rs', lines 104:0-104:50 -/
+   Source: 'tests/src/traits.rs', lines 105:0-105:50 -/
 def h3
   (T1 T2 : Type) (OfTypeInst : OfType T1) (ToTypeInst : ToType T2 T1) 
   (y : T2) :
@@ -171,13 +171,13 @@ def h3
   OfTypeInst.of_type T2 ToTypeInst y
 
 /- Trait declaration: [traits::OfTypeBis]
-   Source: 'tests/src/traits.rs', lines 109:0-109:36 -/
+   Source: 'tests/src/traits.rs', lines 110:0-110:36 -/
 structure OfTypeBis (Self T : Type) where
   ToTypeInst : ToType T Self
   of_type : T → Result Self
 
 /- [traits::h4]:
-   Source: 'tests/src/traits.rs', lines 118:0-118:57 -/
+   Source: 'tests/src/traits.rs', lines 119:0-119:57 -/
 def h4
   (T1 T2 : Type) (OfTypeBisInst : OfTypeBis T1 T2) (ToTypeInst : ToType T2 T1)
   (y : T2) :
@@ -186,33 +186,33 @@ def h4
   OfTypeBisInst.of_type y
 
 /- [traits::TestType]
-   Source: 'tests/src/traits.rs', lines 122:0-122:22 -/
+   Source: 'tests/src/traits.rs', lines 123:0-123:22 -/
 @[reducible] def TestType (T : Type) := T
 
 /- [traits::{traits::TestType<T>#6}::test::TestType1]
-   Source: 'tests/src/traits.rs', lines 127:8-127:24 -/
+   Source: 'tests/src/traits.rs', lines 128:8-128:24 -/
 @[reducible] def TestType.test.TestType1 := U64
 
 /- Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
-   Source: 'tests/src/traits.rs', lines 128:8-128:23 -/
+   Source: 'tests/src/traits.rs', lines 129:8-129:23 -/
 structure TestType.test.TestTrait (Self : Type) where
   test : Self → Result Bool
 
 /- [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}::test]:
-   Source: 'tests/src/traits.rs', lines 139:12-139:34 -/
+   Source: 'tests/src/traits.rs', lines 140:12-140:34 -/
 def TestType.test.TestTraittraitsTestTypetestTestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
   Result.ok (self > 1#u64)
 
 /- Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
-   Source: 'tests/src/traits.rs', lines 138:8-138:36 -/
+   Source: 'tests/src/traits.rs', lines 139:8-139:36 -/
 def TestType.test.TestTraittraitsTestTypetestTestType1 :
   TestType.test.TestTrait TestType.test.TestType1 := {
   test := TestType.test.TestTraittraitsTestTypetestTestType1.test
 }
 
 /- [traits::{traits::TestType<T>#6}::test]:
-   Source: 'tests/src/traits.rs', lines 126:4-126:36 -/
+   Source: 'tests/src/traits.rs', lines 127:4-127:36 -/
 def TestType.test
   (T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
   do
@@ -222,11 +222,11 @@ def TestType.test
   else Result.ok false
 
 /- [traits::BoolWrapper]
-   Source: 'tests/src/traits.rs', lines 150:0-150:22 -/
+   Source: 'tests/src/traits.rs', lines 151:0-151:22 -/
 @[reducible] def BoolWrapper := Bool
 
 /- [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}::to_type]:
-   Source: 'tests/src/traits.rs', lines 156:4-156:25 -/
+   Source: 'tests/src/traits.rs', lines 157:4-157:25 -/
 def ToTypetraitsBoolWrapperT.to_type
   (T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) :
   Result T
@@ -234,21 +234,21 @@ def ToTypetraitsBoolWrapperT.to_type
   ToTypeBoolTInst.to_type self
 
 /- Trait implementation: [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}]
-   Source: 'tests/src/traits.rs', lines 152:0-152:33 -/
+   Source: 'tests/src/traits.rs', lines 153:0-153:33 -/
 def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
   ToType BoolWrapper T := {
   to_type := ToTypetraitsBoolWrapperT.to_type T ToTypeBoolTInst
 }
 
 /- [traits::WithConstTy::LEN2]
-   Source: 'tests/src/traits.rs', lines 164:4-164:21 -/
+   Source: 'tests/src/traits.rs', lines 165:4-165:21 -/
 def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
   Result.ok 32#usize
 def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
   eval_global (WithConstTy.LEN2_default_body Self LEN)
 
 /- Trait declaration: [traits::WithConstTy]
-   Source: 'tests/src/traits.rs', lines 161:0-161:39 -/
+   Source: 'tests/src/traits.rs', lines 162:0-162:39 -/
 structure WithConstTy (Self : Type) (LEN : Usize) where
   LEN1 : Usize
   LEN2 : Usize
@@ -258,17 +258,17 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
   f : W → Array U8 LEN → Result W
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
-   Source: 'tests/src/traits.rs', lines 175:4-175:21 -/
+   Source: 'tests/src/traits.rs', lines 176:4-176:21 -/
 def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize
 def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
-   Source: 'tests/src/traits.rs', lines 180:4-180:39 -/
+   Source: 'tests/src/traits.rs', lines 181:4-181:39 -/
 def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
   Result.ok i
 
 /- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
-   Source: 'tests/src/traits.rs', lines 174:0-174:29 -/
+   Source: 'tests/src/traits.rs', lines 175:0-175:29 -/
 def WithConstTyBool32 : WithConstTy Bool 32#usize := {
   LEN1 := WithConstTyBool32.LEN1
   LEN2 := WithConstTy.LEN2_default Bool 32#usize
@@ -279,7 +279,7 @@ def WithConstTyBool32 : WithConstTy Bool 32#usize := {
 }
 
 /- [traits::use_with_const_ty1]:
-   Source: 'tests/src/traits.rs', lines 183:0-183:75 -/
+   Source: 'tests/src/traits.rs', lines 184:0-184:75 -/
 def use_with_const_ty1
   (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN) :
   Result Usize
@@ -287,7 +287,7 @@ def use_with_const_ty1
   Result.ok WithConstTyInst.LEN1
 
 /- [traits::use_with_const_ty2]:
-   Source: 'tests/src/traits.rs', lines 187:0-187:73 -/
+   Source: 'tests/src/traits.rs', lines 188:0-188:73 -/
 def use_with_const_ty2
   (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
   (w : WithConstTyInst.W) :
@@ -296,7 +296,7 @@ def use_with_const_ty2
   Result.ok ()
 
 /- [traits::use_with_const_ty3]:
-   Source: 'tests/src/traits.rs', lines 189:0-189:80 -/
+   Source: 'tests/src/traits.rs', lines 190:0-190:80 -/
 def use_with_const_ty3
   (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
   (x : WithConstTyInst.W) :
@@ -305,12 +305,12 @@ def use_with_const_ty3
   WithConstTyInst.W_clause_0.to_u64 x
 
 /- [traits::test_where1]:
-   Source: 'tests/src/traits.rs', lines 193:0-193:40 -/
+   Source: 'tests/src/traits.rs', lines 194:0-194:40 -/
 def test_where1 (T : Type) (_x : T) : Result Unit :=
   Result.ok ()
 
 /- [traits::test_where2]:
-   Source: 'tests/src/traits.rs', lines 194:0-194:57 -/
+   Source: 'tests/src/traits.rs', lines 195:0-195:57 -/
 def test_where2
   (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
   Result Unit
@@ -318,30 +318,30 @@ def test_where2
   Result.ok ()
 
 /- Trait declaration: [traits::ParentTrait0]
-   Source: 'tests/src/traits.rs', lines 200:0-200:22 -/
+   Source: 'tests/src/traits.rs', lines 201:0-201:22 -/
 structure ParentTrait0 (Self : Type) where
   W : Type
   get_name : Self → Result String
   get_w : Self → Result W
 
 /- Trait declaration: [traits::ParentTrait1]
-   Source: 'tests/src/traits.rs', lines 205:0-205:22 -/
+   Source: 'tests/src/traits.rs', lines 206:0-206:22 -/
 structure ParentTrait1 (Self : Type) where
 
 /- Trait declaration: [traits::ChildTrait]
-   Source: 'tests/src/traits.rs', lines 206:0-206:49 -/
+   Source: 'tests/src/traits.rs', lines 207:0-207:49 -/
 structure ChildTrait (Self : Type) where
   ParentTrait0Inst : ParentTrait0 Self
   ParentTrait1Inst : ParentTrait1 Self
 
 /- [traits::test_child_trait1]:
-   Source: 'tests/src/traits.rs', lines 209:0-209:56 -/
+   Source: 'tests/src/traits.rs', lines 210:0-210:56 -/
 def test_child_trait1
   (T : Type) (ChildTraitInst : ChildTrait T) (x : T) : Result String :=
   ChildTraitInst.ParentTrait0Inst.get_name x
 
 /- [traits::test_child_trait2]:
-   Source: 'tests/src/traits.rs', lines 213:0-213:54 -/
+   Source: 'tests/src/traits.rs', lines 214:0-214:54 -/
 def test_child_trait2
   (T : Type) (ChildTraitInst : ChildTrait T) (x : T) :
   Result ChildTraitInst.ParentTrait0Inst.W
@@ -349,7 +349,7 @@ def test_child_trait2
   ChildTraitInst.ParentTrait0Inst.get_w x
 
 /- [traits::order1]:
-   Source: 'tests/src/traits.rs', lines 219:0-219:59 -/
+   Source: 'tests/src/traits.rs', lines 220:0-220:59 -/
 def order1
   (T U : Type) (ParentTrait0Inst : ParentTrait0 T) (ParentTrait0Inst1 :
   ParentTrait0 U) :
@@ -358,28 +358,28 @@ def order1
   Result.ok ()
 
 /- Trait declaration: [traits::ChildTrait1]
-   Source: 'tests/src/traits.rs', lines 222:0-222:35 -/
+   Source: 'tests/src/traits.rs', lines 223:0-223:35 -/
 structure ChildTrait1 (Self : Type) where
   ParentTrait1Inst : ParentTrait1 Self
 
 /- Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}]
-   Source: 'tests/src/traits.rs', lines 224:0-224:27 -/
+   Source: 'tests/src/traits.rs', lines 225:0-225:27 -/
 def ParentTrait1Usize : ParentTrait1 Usize := {
 }
 
 /- Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}]
-   Source: 'tests/src/traits.rs', lines 225:0-225:26 -/
+   Source: 'tests/src/traits.rs', lines 226:0-226:26 -/
 def ChildTrait1Usize : ChildTrait1 Usize := {
   ParentTrait1Inst := ParentTrait1Usize
 }
 
 /- Trait declaration: [traits::Iterator]
-   Source: 'tests/src/traits.rs', lines 229:0-229:18 -/
+   Source: 'tests/src/traits.rs', lines 230:0-230:18 -/
 structure Iterator (Self : Type) where
   Item : Type
 
 /- Trait declaration: [traits::IntoIterator]
-   Source: 'tests/src/traits.rs', lines 233:0-233:22 -/
+   Source: 'tests/src/traits.rs', lines 234:0-234:22 -/
 structure IntoIterator (Self : Type) where
   Item : Type
   IntoIter : Type
@@ -387,106 +387,106 @@ structure IntoIterator (Self : Type) where
   into_iter : Self → Result IntoIter
 
 /- Trait declaration: [traits::FromResidual]
-   Source: 'tests/src/traits.rs', lines 250:0-250:21 -/
+   Source: 'tests/src/traits.rs', lines 251:0-251:21 -/
 structure FromResidual (Self T : Type) where
 
 /- Trait declaration: [traits::Try]
-   Source: 'tests/src/traits.rs', lines 246:0-246:48 -/
+   Source: 'tests/src/traits.rs', lines 247:0-247:48 -/
 structure Try (Self : Type) where
   Residual : Type
   FromResidualSelftraitsTryResidualInst : FromResidual Self Residual
 
 /- Trait declaration: [traits::WithTarget]
-   Source: 'tests/src/traits.rs', lines 252:0-252:20 -/
+   Source: 'tests/src/traits.rs', lines 253:0-253:20 -/
 structure WithTarget (Self : Type) where
   Target : Type
 
 /- Trait declaration: [traits::ParentTrait2]
-   Source: 'tests/src/traits.rs', lines 256:0-256:22 -/
+   Source: 'tests/src/traits.rs', lines 257:0-257:22 -/
 structure ParentTrait2 (Self : Type) where
   U : Type
   U_clause_0 : WithTarget U
 
 /- Trait declaration: [traits::ChildTrait2]
-   Source: 'tests/src/traits.rs', lines 260:0-260:35 -/
+   Source: 'tests/src/traits.rs', lines 261:0-261:35 -/
 structure ChildTrait2 (Self : Type) where
   ParentTrait2Inst : ParentTrait2 Self
   convert : ParentTrait2Inst.U → Result ParentTrait2Inst.U_clause_0.Target
 
 /- Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
-   Source: 'tests/src/traits.rs', lines 264:0-264:23 -/
+   Source: 'tests/src/traits.rs', lines 265:0-265:23 -/
 def WithTargetU32 : WithTarget U32 := {
   Target := U32
 }
 
 /- Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}]
-   Source: 'tests/src/traits.rs', lines 268:0-268:25 -/
+   Source: 'tests/src/traits.rs', lines 269:0-269:25 -/
 def ParentTrait2U32 : ParentTrait2 U32 := {
   U := U32
   U_clause_0 := WithTargetU32
 }
 
 /- [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
-   Source: 'tests/src/traits.rs', lines 273:4-273:29 -/
+   Source: 'tests/src/traits.rs', lines 274:4-274:29 -/
 def ChildTrait2U32.convert (x : U32) : Result U32 :=
   Result.ok x
 
 /- Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
-   Source: 'tests/src/traits.rs', lines 272:0-272:24 -/
+   Source: 'tests/src/traits.rs', lines 273:0-273:24 -/
 def ChildTrait2U32 : ChildTrait2 U32 := {
   ParentTrait2Inst := ParentTrait2U32
   convert := ChildTrait2U32.convert
 }
 
 /- Trait declaration: [traits::CFnOnce]
-   Source: 'tests/src/traits.rs', lines 286:0-286:23 -/
+   Source: 'tests/src/traits.rs', lines 287:0-287:23 -/
 structure CFnOnce (Self Args : Type) where
   Output : Type
   call_once : Self → Args → Result Output
 
 /- Trait declaration: [traits::CFnMut]
-   Source: 'tests/src/traits.rs', lines 292:0-292:37 -/
+   Source: 'tests/src/traits.rs', lines 293:0-293:37 -/
 structure CFnMut (Self Args : Type) where
   CFnOnceInst : CFnOnce Self Args
   call_mut : Self → Args → Result (CFnOnceInst.Output × Self)
 
 /- Trait declaration: [traits::CFn]
-   Source: 'tests/src/traits.rs', lines 296:0-296:33 -/
+   Source: 'tests/src/traits.rs', lines 297:0-297:33 -/
 structure CFn (Self Args : Type) where
   CFnMutInst : CFnMut Self Args
   call : Self → Args → Result CFnMutInst.CFnOnceInst.Output
 
 /- Trait declaration: [traits::GetTrait]
-   Source: 'tests/src/traits.rs', lines 300:0-300:18 -/
+   Source: 'tests/src/traits.rs', lines 301:0-301:18 -/
 structure GetTrait (Self : Type) where
   W : Type
   get_w : Self → Result W
 
 /- [traits::test_get_trait]:
-   Source: 'tests/src/traits.rs', lines 305:0-305:49 -/
+   Source: 'tests/src/traits.rs', lines 306:0-306:49 -/
 def test_get_trait
   (T : Type) (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W :=
   GetTraitInst.get_w x
 
 /- Trait declaration: [traits::Trait]
-   Source: 'tests/src/traits.rs', lines 310:0-310:15 -/
+   Source: 'tests/src/traits.rs', lines 311:0-311:15 -/
 structure Trait (Self : Type) where
   LEN : Usize
 
 /- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
-   Source: 'tests/src/traits.rs', lines 315:4-315:20 -/
+   Source: 'tests/src/traits.rs', lines 316:4-316:20 -/
 def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
 def TraitArray.LEN (T : Type) (N : Usize) : Usize :=
   eval_global (TraitArray.LEN_body T N)
 
 /- Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}]
-   Source: 'tests/src/traits.rs', lines 314:0-314:40 -/
+   Source: 'tests/src/traits.rs', lines 315:0-315:40 -/
 def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
   LEN := TraitArray.LEN T N
 }
 
 /- [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN]
-   Source: 'tests/src/traits.rs', lines 319:4-319:20 -/
+   Source: 'tests/src/traits.rs', lines 320:4-320:20 -/
 def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
   : Result Usize :=
   Result.ok 0#usize
@@ -494,19 +494,19 @@ def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
   eval_global (TraittraitsWrapper.LEN_body T TraitInst)
 
 /- Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}]
-   Source: 'tests/src/traits.rs', lines 318:0-318:35 -/
+   Source: 'tests/src/traits.rs', lines 319:0-319:35 -/
 def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T)
   := {
   LEN := TraittraitsWrapper.LEN T TraitInst
 }
 
 /- [traits::use_wrapper_len]:
-   Source: 'tests/src/traits.rs', lines 322:0-322:43 -/
+   Source: 'tests/src/traits.rs', lines 323:0-323:43 -/
 def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize :=
   Result.ok (TraittraitsWrapper T TraitInst).LEN
 
 /- [traits::Foo]
-   Source: 'tests/src/traits.rs', lines 326:0-326:20 -/
+   Source: 'tests/src/traits.rs', lines 327:0-327:20 -/
 structure Foo (T U : Type) where
   x : T
   y : U
@@ -519,7 +519,7 @@ inductive core.result.Result (T E : Type) :=
 | Err : E → core.result.Result T E
 
 /- [traits::{traits::Foo<T, U>#16}::FOO]
-   Source: 'tests/src/traits.rs', lines 332:4-332:33 -/
+   Source: 'tests/src/traits.rs', lines 333:4-333:33 -/
 def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
   : Result (core.result.Result T I32) :=
   Result.ok (core.result.Result.Err 0#i32)
@@ -527,13 +527,13 @@ def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
   eval_global (Foo.FOO_body T U TraitInst)
 
 /- [traits::use_foo1]:
-   Source: 'tests/src/traits.rs', lines 335:0-335:48 -/
+   Source: 'tests/src/traits.rs', lines 336:0-336:48 -/
 def use_foo1
   (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) :=
   Result.ok (Foo.FOO T U TraitInst)
 
 /- [traits::use_foo2]:
-   Source: 'tests/src/traits.rs', lines 339:0-339:48 -/
+   Source: 'tests/src/traits.rs', lines 340:0-340:48 -/
 def use_foo2
   (T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) :=
   Result.ok (Foo.FOO U T TraitInst)
diff --git a/tests/lean/lakefile.lean b/tests/lean/lakefile.lean
index 3a777824..ba336a4a 100644
--- a/tests/lean/lakefile.lean
+++ b/tests/lean/lakefile.lean
@@ -9,11 +9,10 @@ require base from "../../backends/lean"
 package «tests» {}
 
 @[default_target] lean_lib Tutorial
-@[default_target] lean_lib BetreeMain
+@[default_target] lean_lib Betree
 @[default_target] lean_lib Constants
 @[default_target] lean_lib External
 @[default_target] lean_lib Hashmap
-@[default_target] lean_lib HashmapMain
 @[default_target] lean_lib Loops
 @[default_target] lean_lib NoNestedBorrows
 @[default_target] lean_lib Paper
diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean
new file mode 100644
index 00000000..b0fcb9e9
--- /dev/null
+++ b/tests/lean/misc/MutuallyRecursiveTraits.lean
@@ -0,0 +1,6 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [mutually_recursive_traits]
+import Base
+open Primitives
+
+namespace mutually_recursive_traits