Merge pull request #206 from AeneasVerif/subdir

8 files changed, 177 insertions, 177 deletions

diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 3c381233..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 4:0-4: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 11:0-11: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 18:0-18: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 22:0-22: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 26:0-26: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 334f4707..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 7:0-7: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 9:0-9: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 12:0-12: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 19:0-19: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 17:0-17: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 25:0-25: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 38:0-38: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 29:0-29: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 33:0-33: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 34:0-34: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 35:0-35: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 36:0-36: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 51:0-51: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 56:4-56: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 43:0-43: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 45:0-45: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 49:0-49: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 64:4-64: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 63:0-63: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 68:0-68: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 76:0-76: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 77:0-77: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 78:0-78: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 72:0-72: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 82:0-82: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 83:0-83: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 84:0-84: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 85:0-85: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 88:0-88: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 93:4-93: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 96:0-96: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 a7683eb0..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 6:0-6: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 14:0-14: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 18:0-18: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 22:0-22: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 26:0-26: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 35:0-35: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 40:0-40: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 55:0-55: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 70:0-79: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 70:0-70: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 81:0-81: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 89:0-89: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 98:0-98: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 103:4-103: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 102:0-102: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 110:0-110: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 84fe1a28..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 8:0-8: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 12:0-12: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/Loops.lean b/tests/lean/Loops.lean
index 54f1b24f..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 7:0-17: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 7:0-7: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 22:0-34: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 22:0-22: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 37:0-51: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 37:0-37: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 53:0-61: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 53:0-53: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 65:0-71: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 65:0-65: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 73:0-73: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 79:0-88: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 79:0-79: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 91:0-101: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 91:0-91: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 104:0-114: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 104:0-104: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 116:0-130: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 116:0-116: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 132:0-146: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 132:0-132: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 148:0-148: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 152:0-152: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 157:0-168: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 157:0-157: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 171:0-182: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 171:0-171: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 187:0-208: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 187:0-191: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 211:0-232: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 211:0-215: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 236:0-251: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 236:0-240: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 254:0-269: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 254:0-258: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 272:0-287: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 272:0-276: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 291:0-306: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 291:0-295: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 310:0-325: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 310:0-314: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 329:0-344: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 329:0-333: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 348:0-352: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 348:0-348: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 356:0-361: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 356:0-356: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 365:0-369: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 365:0-365: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/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1781ac71..022b32fb 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 6:0-6: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 11:0-11: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 22:0-22: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 28:0-28: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 34:0-34: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 41:0-41: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 43:0-43: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 48:0-48: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 52:0-52: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 57:0-57: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 62:0-62: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 74:0-74: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 82:0-82: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 89:0-89: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 96:0-96: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 107:0-107: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 123:0-123: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 128:0-128: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 138:0-138: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 144:0-144: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 152:0-152: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 159:0-159: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 166:0-166: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 173:0-173: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 179:0-179: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 187:0-187: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 194:0-194: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 202:0-202: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,20 +254,20 @@ def choose_test : Result Unit :=
 #assert (choose_test == Result.ok ())
 
 /- [no_nested_borrows::test_char]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 214:0-214:26 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 215:0-215:26 -/
 def test_char : Result Char :=
   Result.ok 'a'
 
 mutual
 
 /- [no_nested_borrows::Tree]
-   Source: 'tests/src/no_nested_borrows.rs', lines 219:0-219:16 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 220:0-220: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 224:0-224:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 225:0-225:20 -/
 inductive NodeElem (T : Type) :=
 | Cons : Tree T → NodeElem T → NodeElem T
 | Nil : NodeElem T
@@ -275,7 +275,7 @@ inductive NodeElem (T : Type) :=
 end
 
 /- [no_nested_borrows::list_length]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 259:0-259:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 260:0-260:48 -/
 divergent def list_length (T : Type) (l : List T) : Result U32 :=
   match l with
   | List.Cons _ l1 => do
@@ -284,7 +284,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 267:0-267:62 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 268:0-268:62 -/
 divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
@@ -296,7 +296,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 283:0-283:67 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 284:0-284:67 -/
 divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
@@ -318,7 +318,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 299:0-299:63 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 300:0-300:63 -/
 divergent def list_rev_aux
   (T : Type) (li : List T) (lo : List T) : Result (List T) :=
   match li with
@@ -326,13 +326,13 @@ divergent def list_rev_aux
   | List.Nil => Result.ok lo
 
 /- [no_nested_borrows::list_rev]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 313:0-313:42 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 314:0-314: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 318:0-318:28 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 319:0-319:28 -/
 def test_list_functions : Result Unit :=
   do
   let l := List.Cons 2#i32 List.Nil
@@ -379,7 +379,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 334:0-334:89 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 335:0-335:89 -/
 def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -387,7 +387,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 338:0-338:88 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 339:0-339:88 -/
 def id_mut_pair2
   (T1 T2 : Type) (p : (T1 × T2)) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -396,7 +396,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 342:0-342:93 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 343:0-343:93 -/
 def id_mut_pair3
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -404,7 +404,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 346:0-346:92 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 347:0-347:92 -/
 def id_mut_pair4
   (T1 T2 : Type) (p : (T1 × T2)) :
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -413,37 +413,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 353:0-353:34 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 354:0-354:34 -/
 structure StructWithTuple (T1 T2 : Type) where
   p : (T1 × T2)
 
 /- [no_nested_borrows::new_tuple1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 357:0-357:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 358:0-358: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 361:0-361:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 362:0-362: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 365:0-365:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 366:0-366: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 370:0-370:33 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:33 -/
 structure StructWithPair (T1 T2 : Type) where
   p : Pair T1 T2
 
 /- [no_nested_borrows::new_pair1]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 374:0-374:46 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 375:0-375: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 382:0-382:23 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 383:0-383:23 -/
 def test_constants : Result Unit :=
   do
   let swt ← new_tuple1
@@ -473,7 +473,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 391:0-391:28 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 392:0-392:28 -/
 def test_weird_borrows1 : Result Unit :=
   Result.ok ()
 
@@ -481,7 +481,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 401:0-401:37 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 402:0-402:37 -/
 def test_mem_replace (px : U32) : Result U32 :=
   let (y, _) := core.mem.replace U32 px 1#u32
   if ¬ (y = 0#u32)
@@ -489,71 +489,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 408:0-408:47 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 409:0-409: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 421:0-421:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 422:0-422: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 436:0-436:52 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 437:0-437: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 448:0-448:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 449:0-449:40 -/
 def test_shared_borrow_enum2 : Result U32 :=
   Result.ok 0#u32
 
 /- [no_nested_borrows::incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 459:0-459:24 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 460:0-460:24 -/
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
 /- [no_nested_borrows::call_incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 463:0-463:35 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 464:0-464:35 -/
 def call_incr (x : U32) : Result U32 :=
   incr x
 
 /- [no_nested_borrows::read_then_incr]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 468:0-468:41 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469: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 474:0-474:24 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 475:0-475:24 -/
 def Tuple (T1 T2 : Type) := T1 × T2
 
 /- [no_nested_borrows::use_tuple_struct]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 476:0-476:48 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 477:0-477: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 480:0-480:61 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 481:0-481: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 485:0-485:20 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:20 -/
 @[reducible] def IdType (T : Type) := T
 
 /- [no_nested_borrows::use_id_type]:
-   Source: 'tests/src/no_nested_borrows.rs', lines 487:0-487:40 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 488:0-488: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 491:0-491:43 -/
+   Source: 'tests/src/no_nested_borrows.rs', lines 492:0-492: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 e98ada42..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 6:0-6: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 10:0-10: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 17:0-17: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 25:0-25: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 37:0-37: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 44:0-44: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 59:0-59: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 70:0-70: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 78:0-78: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 defa48c7..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 5:0-5: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 15:0-15: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)))