Revert "Regenerate the tests"

This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.

12 files changed, 338 insertions, 333 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 70b4a26b..9748919e 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -14,34 +14,34 @@ inductive AB :=
 /- [arrays::incr]:
    Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/
 def incr (x : U32) : Result U32 :=
-  x + 1u32
+  x + 1#u32
 
 /- [arrays::array_to_shared_slice_]:
    Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/
 def array_to_shared_slice_
-  (T : Type) (s : Array T 32usize) : Result (Slice T) :=
-  Array.to_slice T 32usize s
+  (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 24:0-24:58 -/
 def array_to_mut_slice_
-  (T : Type) (s : Array T 32usize) :
-  Result ((Slice T) × (Slice T → Result (Array T 32usize)))
+  (T : Type) (s : Array T 32#usize) :
+  Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
   :=
-  Array.to_slice_mut T 32usize s
+  Array.to_slice_mut T 32#usize s
 
 /- [arrays::array_len]:
    Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/
-def array_len (T : Type) (s : Array T 32usize) : Result Usize :=
+def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
-  let s1 ← Array.to_slice T 32usize s
+  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 32:0-32:48 -/
-def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize :=
+def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
-  let s1 ← Array.to_slice T 32usize s
+  let s1 ← Array.to_slice T 32#usize s
   Result.ok (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
@@ -52,26 +52,26 @@ def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
 /- [arrays::index_array_shared]:
    Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/
 def index_array_shared
-  (T : Type) (s : Array T 32usize) (i : Usize) : Result T :=
-  Array.index_usize T 32usize s i
+  (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 47:0-47:53 -/
-def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 :=
-  Array.index_usize U32 32usize s i
+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 51:0-51:45 -/
-def index_array_copy (x : Array U32 32usize) : Result U32 :=
-  Array.index_usize U32 32usize x 0usize
+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 55:0-55:62 -/
 def index_mut_array
-  (T : Type) (s : Array T 32usize) (i : Usize) :
-  Result (T × (T → Result (Array T 32usize)))
+  (T : Type) (s : Array T 32#usize) (i : Usize) :
+  Result (T × (T → Result (Array T 32#usize)))
   :=
-  Array.index_mut_usize T 32usize s i
+  Array.index_mut_usize T 32#usize s i
 
 /- [arrays::index_slice]:
    Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/
@@ -109,22 +109,22 @@ def slice_subslice_mut_
 
 /- [arrays::array_to_slice_shared_]:
    Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/
-def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) :=
-  Array.to_slice U32 32usize x
+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 79:0-79:59 -/
 def array_to_slice_mut_
-  (x : Array U32 32usize) :
-  Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
+  (x : Array U32 32#usize) :
+  Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
   :=
-  Array.to_slice_mut U32 32usize x
+  Array.to_slice_mut U32 32#usize x
 
 /- [arrays::array_subslice_shared_]:
    Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/
 def array_subslice_shared_
-  (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
-  core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
+  (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)
     (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
     { start := y, end_ := z }
@@ -132,12 +132,12 @@ def array_subslice_shared_
 /- [arrays::array_subslice_mut_]:
    Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/
 def array_subslice_mut_
-  (x : Array U32 32usize) (y : Usize) (z : Usize) :
-  Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
+  (x : Array U32 32#usize) (y : Usize) (z : Usize) :
+  Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
   :=
   do
   let (s, index_mut_back) ←
-    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize
+    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize
       (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
       (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
       { start := y, end_ := z }
@@ -146,50 +146,50 @@ def array_subslice_mut_
 /- [arrays::index_slice_0]:
    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 0usize
+  Slice.index_usize T s 0#usize
 
 /- [arrays::index_array_0]:
    Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/
-def index_array_0 (T : Type) (s : Array T 32usize) : Result T :=
-  Array.index_usize T 32usize s 0usize
+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 106:0-106:71 -/
 def index_index_array
-  (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
+  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
   Result U32
   :=
   do
-  let a ← Array.index_usize (Array U32 32usize) 32usize s i
-  Array.index_usize U32 32usize a j
+  let a ← Array.index_usize (Array U32 32#usize) 32#usize s i
+  Array.index_usize U32 32#usize a j
 
 /- [arrays::update_update_array]:
    Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/
 def update_update_array
-  (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
+  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
   Result Unit
   :=
   do
   let (a, index_mut_back) ←
-    Array.index_mut_usize (Array U32 32usize) 32usize s i
-  let (_, index_mut_back1) ← Array.index_mut_usize U32 32usize a j
-  let a1 ← index_mut_back1 0u32
+    Array.index_mut_usize (Array U32 32#usize) 32#usize s i
+  let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j
+  let a1 ← index_mut_back1 0#u32
   let _ ← index_mut_back a1
   Result.ok ()
 
 /- [arrays::array_local_deep_copy]:
    Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/
-def array_local_deep_copy (x : Array U32 32usize) : Result Unit :=
+def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_array]:
    Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/
-def take_array (a : Array U32 2usize) : Result Unit :=
+def take_array (a : Array U32 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_array_borrow]:
    Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/
-def take_array_borrow (a : Array U32 2usize) : Result Unit :=
+def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_slice]:
@@ -204,67 +204,70 @@ def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
 
 /- [arrays::const_array]:
    Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/
-def const_array : Result (Array U32 2usize) :=
-  Result.ok (Array.make U32 2usize [ 0u32, 0u32 ])
+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 134:0-134:20 -/
 def const_slice : Result Unit :=
   do
-  let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+  let _ ←
+    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   Result.ok ()
 
 /- [arrays::take_all]:
    Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/
 def take_all : Result Unit :=
   do
-  let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ])
-  let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ])
-  let _ ← take_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
-  let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+  let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let s ←
+    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let _ ← take_slice s
   let (s1, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let s2 ← take_mut_slice s1
   let _ ← to_slice_mut_back s2
   Result.ok ()
 
 /- [arrays::index_array]:
    Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/
-def index_array (x : Array U32 2usize) : Result U32 :=
-  Array.index_usize U32 2usize x 0usize
+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 161:0-161:46 -/
-def index_array_borrow (x : Array U32 2usize) : Result U32 :=
-  Array.index_usize U32 2usize x 0usize
+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 165:0-165:42 -/
 def index_slice_u32_0 (x : Slice U32) : Result U32 :=
-  Slice.index_usize U32 x 0usize
+  Slice.index_usize U32 x 0#usize
 
 /- [arrays::index_mut_slice_u32_0]:
    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 0usize
+  let i ← Slice.index_usize U32 x 0#usize
   Result.ok (i, x)
 
 /- [arrays::index_all]:
    Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/
 def index_all : Result U32 :=
   do
-  let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
-  let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
+  let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let i2 ← i + i1
-  let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
+  let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let i4 ← i2 + i3
-  let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+  let s ←
+    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let i5 ← index_slice_u32_0 s
   let i6 ← i4 + i5
   let (s1, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
   let i8 ← i6 + i7
   let _ ← to_slice_mut_back s2
@@ -272,35 +275,35 @@ def index_all : Result U32 :=
 
 /- [arrays::update_array]:
    Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
-def update_array (x : Array U32 2usize) : Result Unit :=
+def update_array (x : Array U32 2#usize) : Result Unit :=
   do
-  let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
-  let _ ← index_mut_back 1u32
+  let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
+  let _ ← index_mut_back 1#u32
   Result.ok ()
 
 /- [arrays::update_array_mut_borrow]:
    Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/
 def update_array_mut_borrow
-  (x : Array U32 2usize) : Result (Array U32 2usize) :=
+  (x : Array U32 2#usize) : Result (Array U32 2#usize) :=
   do
-  let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
-  index_mut_back 1u32
+  let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
+  index_mut_back 1#u32
 
 /- [arrays::update_mut_slice]:
    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 0usize
-  index_mut_back 1u32
+  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 197:0-197:19 -/
 def update_all : Result Unit :=
   do
-  let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ])
-  let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ])
-  let x ← update_array_mut_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
-  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2usize x
+  let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
   let s1 ← update_mut_slice s
   let _ ← to_slice_mut_back s1
   Result.ok ()
@@ -310,37 +313,37 @@ def update_all : Result Unit :=
 def range_all : Result Unit :=
   do
   let (s, index_mut_back) ←
-    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize
+    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize
       (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
       (core.slice.index.SliceIndexRangeUsizeSliceTInst U32))
-      (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ])
-      { start := 1usize, end_ := 3usize }
+      (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ])
+      { start := 1#usize, end_ := 3#usize }
   let s1 ← update_mut_slice s
   let _ ← index_mut_back s1
   Result.ok ()
 
 /- [arrays::deref_array_borrow]:
    Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/
-def deref_array_borrow (x : Array U32 2usize) : Result U32 :=
-  Array.index_usize U32 2usize x 0usize
+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 222:0-222:54 -/
 def deref_array_mut_borrow
-  (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) :=
+  (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
   do
-  let i ← Array.index_usize U32 2usize x 0usize
+  let i ← Array.index_usize U32 2#usize x 0#usize
   Result.ok (i, x)
 
 /- [arrays::take_array_t]:
    Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/
-def take_array_t (a : Array AB 2usize) : Result Unit :=
+def take_array_t (a : Array AB 2#usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::non_copyable_array]:
    Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/
 def non_copyable_array : Result Unit :=
-  take_array_t (Array.make AB 2usize [ AB.A, AB.B ])
+  take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
    Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
@@ -351,14 +354,14 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
     do
     let i2 ← Slice.index_usize U32 s i
     let sum3 ← sum1 + i2
-    let i3 ← i + 1usize
+    let i3 ← i + 1#usize
     sum_loop s sum3 i3
   else Result.ok sum1
 
 /- [arrays::sum]:
    Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/
 def sum (s : Slice U32) : Result U32 :=
-  sum_loop s 0u32 0usize
+  sum_loop s 0#u32 0#usize
 
 /- [arrays::sum2]: loop 0:
    Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
@@ -372,7 +375,7 @@ divergent def sum2_loop
     let i3 ← Slice.index_usize U32 s2 i
     let i4 ← i2 + i3
     let sum3 ← sum1 + i4
-    let i5 ← i + 1usize
+    let i5 ← i + 1#usize
     sum2_loop s s2 sum3 i5
   else Result.ok sum1
 
@@ -382,7 +385,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
   let i := Slice.len U32 s
   let i1 := Slice.len U32 s2
   if i = i1
-  then sum2_loop s s2 0u32 0usize
+  then sum2_loop s s2 0#u32 0#usize
   else Result.fail .panic
 
 /- [arrays::f0]:
@@ -390,9 +393,9 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
 def f0 : Result Unit :=
   do
   let (s, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
-  let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0usize
-  let s1 ← index_mut_back 1u32
+    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+  let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize
+  let s1 ← index_mut_back 1#u32
   let _ ← to_slice_mut_back s1
   Result.ok ()
 
@@ -401,9 +404,9 @@ def f0 : Result Unit :=
 def f1 : Result Unit :=
   do
   let (_, index_mut_back) ←
-    Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
-      0usize
-  let _ ← index_mut_back 1u32
+    Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+      0#usize
+  let _ ← index_mut_back 1#u32
   Result.ok ()
 
 /- [arrays::f2]:
@@ -413,8 +416,8 @@ def f2 (i : U32) : Result Unit :=
 
 /- [arrays::f4]:
    Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/
-def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
-  core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
+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)
     (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
     { start := y, end_ := z }
@@ -424,32 +427,34 @@ def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
 def f3 : Result U32 :=
   do
   let i ←
-    Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize
+    Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+      0#usize
   let _ ← f2 i
-  let b := Array.repeat U32 32usize 0u32
-  let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
-  let s1 ← f4 b 16usize 18usize
+  let b := Array.repeat U32 32#usize 0#u32
+  let s ←
+    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+  let s1 ← f4 b 16#usize 18#usize
   sum2 s s1
 
 /- [arrays::SZ]
    Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/
-def SZ_body : Result Usize := Result.ok 32usize
+def SZ_body : Result Usize := Result.ok 32#usize
 def SZ : Usize := eval_global SZ_body
 
 /- [arrays::f5]:
    Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/
-def f5 (x : Array U32 32usize) : Result U32 :=
-  Array.index_usize U32 32usize x 0usize
+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 297:0-297:12 -/
 def ite : Result Unit :=
   do
   let (s, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let (_, s1) ← index_mut_slice_u32_0 s
   let (s2, to_slice_mut_back1) ←
-    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
   let (_, s3) ← index_mut_slice_u32_0 s2
   let _ ← to_slice_mut_back1 s3
   let _ ← to_slice_mut_back s1
@@ -463,8 +468,8 @@ divergent def zero_slice_loop
   then
     do
     let (_, index_mut_back) ← Slice.index_mut_usize U8 a i
-    let i1 ← i + 1usize
-    let a1 ← index_mut_back 0u8
+    let i1 ← i + 1#usize
+    let a1 ← index_mut_back 0#u8
     zero_slice_loop a1 i1 len
   else Result.ok a
 
@@ -472,14 +477,14 @@ divergent def zero_slice_loop
    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 0usize len
+  zero_slice_loop a 0#usize len
 
 /- [arrays::iter_mut_slice]: loop 0:
    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
-       let i1 ← i + 1usize
+       let i1 ← i + 1#usize
        iter_mut_slice_loop len i1
   else Result.ok ()
 
@@ -488,7 +493,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
 def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   do
   let len := Slice.len U8 a
-  let _ ← iter_mut_slice_loop len 0usize
+  let _ ← iter_mut_slice_loop len 0#usize
   Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
@@ -501,7 +506,7 @@ divergent def sum_mut_slice_loop
     do
     let i2 ← Slice.index_usize U32 a i
     let s1 ← s + i2
-    let i3 ← i + 1usize
+    let i3 ← i + 1#usize
     sum_mut_slice_loop a i3 s1
   else Result.ok s
 
@@ -509,7 +514,7 @@ divergent def sum_mut_slice_loop
    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 0usize 0u32
+  let i ← sum_mut_slice_loop a 0#usize 0#u32
   Result.ok (i, a)
 
 end arrays
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 74344e01..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -41,20 +41,20 @@ def betree.store_leaf_node
    Source: 'src/betree.rs', lines 55:0-55:48 -/
 def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
-  let counter1 ← counter + 1u64
+  let counter1 ← counter + 1#u64
   Result.ok (counter, counter1)
 
 /- [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 := 0u64 }
+  Result.ok { next_node_id := 0#u64 }
 
 /- [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) :=
   do
-  let i ← self.next_node_id + 1u64
+  let i ← self.next_node_id + 1#u64
   Result.ok (self.next_node_id, { next_node_id := i })
 
 /- [betree::betree::upsert_update]:
@@ -65,7 +65,7 @@ def betree.upsert_update
   | none =>
     match st with
     | betree.UpsertFunState.Add v => Result.ok v
-    | betree.UpsertFunState.Sub _ => Result.ok 0u64
+    | betree.UpsertFunState.Sub _ => Result.ok 0#u64
   | some prev1 =>
     match st with
     | betree.UpsertFunState.Add v =>
@@ -77,7 +77,7 @@ def betree.upsert_update
     | betree.UpsertFunState.Sub v =>
       if prev1 >= v
       then prev1 - v
-      else Result.ok 0u64
+      else Result.ok 0#u64
 
 /- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
    Source: 'src/betree.rs', lines 276:4-284:5 -/
@@ -86,14 +86,14 @@ divergent def betree.List.len_loop
   match self with
   | betree.List.Cons _ tl =>
     do
-    let len1 ← len + 1u64
+    let len1 ← len + 1#u64
     betree.List.len_loop T tl len1
   | betree.List.Nil => Result.ok len
 
 /- [betree::betree::{betree::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
 def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
-  betree.List.len_loop T self 0u64
+  betree.List.len_loop T self 0#u64
 
 /- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
    Source: 'src/betree.rs', lines 304:4-312:5 -/
@@ -118,12 +118,12 @@ divergent def betree.List.split_at_loop
   (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n > 0u64
+  if n > 0#u64
   then
     match self with
     | betree.List.Cons hd tl =>
       do
-      let n1 ← n - 1u64
+      let n1 ← n - 1#u64
       betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
     | betree.List.Nil => Result.fail .panic
   else do
@@ -706,7 +706,7 @@ divergent def betree.Node.apply_messages
     let (st1, content) ← betree.load_leaf_node node.id st
     let content1 ← betree.Node.apply_messages_to_leaf content msgs
     let len ← betree.List.len (U64 × U64) content1
-    let i ← 2u64 * params.split_size
+    let i ← 2#u64 * params.split_size
     if len >= i
     then
       do
@@ -751,7 +751,7 @@ def betree.BeTree.new
     {
       params := { min_flush_size := min_flush_size, split_size := split_size },
       node_id_cnt := node_id_cnt1,
-      root := (betree.Node.Leaf { id := id, size := 0u64 })
+      root := (betree.Node.Leaf { id := id, size := 0#u64 })
     })
 
 /- [betree::betree::{betree::betree::BeTree#6}::apply]:
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 8884d309..23ec66b4 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -9,15 +9,15 @@ namespace bitwise
    Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/
 def shift_u32 (a : U32) : Result U32 :=
   do
-  let t ← a >>> 16usize
-  t <<< 16usize
+  let t ← a >>> 16#usize
+  t <<< 16#usize
 
 /- [bitwise::shift_i32]:
    Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
 def shift_i32 (a : I32) : Result I32 :=
   do
-  let t ← a >>> 16isize
-  t <<< 16isize
+  let t ← a >>> 16#isize
+  t <<< 16#isize
 
 /- [bitwise::xor_u32]:
    Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index a72ac98d..ecb91c16 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -7,7 +7,7 @@ namespace constants
 
 /- [constants::X0]
    Source: 'tests/src/constants.rs', lines 8:0-8:17 -/
-def X0_body : Result U32 := Result.ok 0u32
+def X0_body : Result U32 := Result.ok 0#u32
 def X0 : U32 := eval_global X0_body
 
 /- [constants::X1]
@@ -17,17 +17,17 @@ def X1 : U32 := eval_global X1_body
 
 /- [constants::X2]
    Source: 'tests/src/constants.rs', lines 13:0-13:17 -/
-def X2_body : Result U32 := Result.ok 3u32
+def X2_body : Result U32 := Result.ok 3#u32
 def X2 : U32 := eval_global X2_body
 
 /- [constants::incr]:
    Source: 'tests/src/constants.rs', lines 20:0-20:32 -/
 def incr (n : U32) : Result U32 :=
-  n + 1u32
+  n + 1#u32
 
 /- [constants::X3]
    Source: 'tests/src/constants.rs', lines 18:0-18:17 -/
-def X3_body : Result U32 := incr 32u32
+def X3_body : Result U32 := incr 32#u32
 def X3 : U32 := eval_global X3_body
 
 /- [constants::mk_pair0]:
@@ -48,22 +48,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
 
 /- [constants::P0]
    Source: 'tests/src/constants.rs', lines 34:0-34:24 -/
-def P0_body : Result (U32 × U32) := mk_pair0 0u32 1u32
+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 35:0-35:28 -/
-def P1_body : Result (Pair U32 U32) := mk_pair1 0u32 1u32
+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 36:0-36:24 -/
-def P2_body : Result (U32 × U32) := Result.ok (0u32, 1u32)
+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 37:0-37:28 -/
-def P3_body : Result (Pair U32 U32) := Result.ok { x := 0u32, y := 1u32 }
+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]
@@ -78,7 +78,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
 
 /- [constants::Y]
    Source: 'tests/src/constants.rs', lines 44:0-44:22 -/
-def Y_body : Result (Wrap I32) := Wrap.new I32 2i32
+def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32
 def Y : Wrap I32 := eval_global Y_body
 
 /- [constants::unwrap_y]:
@@ -93,7 +93,7 @@ def YVAL : I32 := eval_global YVAL_body
 
 /- [constants::get_z1::Z1]
    Source: 'tests/src/constants.rs', lines 65:4-65:17 -/
-def get_z1.Z1_body : Result I32 := Result.ok 3i32
+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]:
@@ -108,7 +108,7 @@ def add (a : I32) (b : I32) : Result I32 :=
 
 /- [constants::Q1]
    Source: 'tests/src/constants.rs', lines 77:0-77:17 -/
-def Q1_body : Result I32 := Result.ok 5i32
+def Q1_body : Result I32 := Result.ok 5#i32
 def Q1 : I32 := eval_global Q1_body
 
 /- [constants::Q2]
@@ -118,7 +118,7 @@ def Q2 : I32 := eval_global Q2_body
 
 /- [constants::Q3]
    Source: 'tests/src/constants.rs', lines 79:0-79:17 -/
-def Q3_body : Result I32 := add Q2 3i32
+def Q3_body : Result I32 := add Q2 3#i32
 def Q3 : I32 := eval_global Q3_body
 
 /- [constants::get_z2]:
@@ -131,7 +131,7 @@ def get_z2 : Result I32 :=
 
 /- [constants::S1]
    Source: 'tests/src/constants.rs', lines 83:0-83:18 -/
-def S1_body : Result U32 := Result.ok 6u32
+def S1_body : Result U32 := Result.ok 6#u32
 def S1 : U32 := eval_global S1_body
 
 /- [constants::S2]
@@ -146,7 +146,7 @@ def S3 : Pair U32 U32 := eval_global S3_body
 
 /- [constants::S4]
    Source: 'tests/src/constants.rs', lines 86:0-86:29 -/
-def S4_body : Result (Pair U32 U32) := mk_pair1 7u32 8u32
+def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
 def S4 : Pair U32 U32 := eval_global S4_body
 
 /- [constants::V]
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 9d8b085c..48ac2062 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -22,7 +22,7 @@ def choose
 def mul2_add1 (x : U32) : Result U32 :=
   do
   let i ← x + x
-  i + 1u32
+  i + 1#u32
 
 /- [demo::use_mul2_add1]:
    Source: 'tests/src/demo.rs', lines 19:0-19:43 -/
@@ -34,13 +34,13 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
 /- [demo::incr]:
    Source: 'tests/src/demo.rs', lines 23:0-23:31 -/
 def incr (x : U32) : Result U32 :=
-  x + 1u32
+  x + 1#u32
 
 /- [demo::use_incr]:
    Source: 'tests/src/demo.rs', lines 27:0-27:17 -/
 def use_incr : Result Unit :=
   do
-  let x ← incr 0u32
+  let x ← incr 0#u32
   let x1 ← incr x
   let _ ← incr x1
   Result.ok ()
@@ -56,10 +56,10 @@ inductive CList (T : Type) :=
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then Result.ok x
     else do
-         let i1 ← i - 1u32
+         let i1 ← i - 1#u32
          list_nth T tl i1
   | CList.CNil => Result.fail .panic
 
@@ -71,13 +71,13 @@ divergent def list_nth_mut
   :=
   match l with
   | CList.CCons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (CList.CCons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
       let back :=
         fun ret =>
@@ -95,13 +95,13 @@ divergent def list_nth_mut1_loop
   :=
   match l with
   | CList.CCons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (CList.CCons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, back) ← list_nth_mut1_loop T tl i1
       let back1 :=
         fun ret => do
@@ -121,12 +121,12 @@ def list_nth_mut1
 /- [demo::i32_id]:
    Source: 'tests/src/demo.rs', lines 82:0-82:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
-  if i = 0i32
-  then Result.ok 0i32
+  if i = 0#i32
+  then Result.ok 0#i32
   else do
-       let i1 ← i - 1i32
+       let i1 ← i - 1#i32
        let i2 ← i32_id i1
-       i2 + 1i32
+       i2 + 1#i32
 
 /- [demo::list_tail]:
    Source: 'tests/src/demo.rs', lines 90:0-90:64 -/
@@ -155,7 +155,7 @@ structure Counter (Self : Type) where
    Source: 'tests/src/demo.rs', lines 104:4-104:31 -/
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
-  let self1 ← self + 1usize
+  let self1 ← self + 1#usize
   Result.ok (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index c828720a..1b1d5cdf 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -27,7 +27,7 @@ def incr
   :=
   do
   let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
-  let i1 ← i + 1u32
+  let i1 ← i + 1#u32
   let (_, rc1) ← get_mut_back i1 st1
   Result.ok (st1, rc1)
 
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 3c244ee0..612e1848 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -18,11 +18,11 @@ divergent def HashMap.allocate_slots_loop
   (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
   Result (alloc.vec.Vec (List T))
   :=
-  if n > 0usize
+  if n > 0#usize
   then
     do
     let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
-    let n1 ← n - 1usize
+    let n1 ← n - 1#usize
     HashMap.allocate_slots_loop T slots1 n1
   else Result.ok slots
 
@@ -47,7 +47,7 @@ def HashMap.new_with_capacity
   let i1 ← i / max_load_divisor
   Result.ok
     {
-      num_entries := 0usize,
+      num_entries := 0#usize,
       max_load_factor := (max_load_dividend, max_load_divisor),
       max_load := i1,
       slots := slots
@@ -56,7 +56,7 @@ def HashMap.new_with_capacity
 /- [hashmap::{hashmap::HashMap<T>}::new]:
    Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/
 def HashMap.new (T : Type) : Result (HashMap T) :=
-  HashMap.new_with_capacity T 32usize 4usize 5usize
+  HashMap.new_with_capacity T 32#usize 4#usize 5#usize
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
    Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/
@@ -71,7 +71,7 @@ divergent def HashMap.clear_loop
     let (_, index_mut_back) ←
       alloc.vec.Vec.index_mut (List T) Usize
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
-    let i2 ← i + 1usize
+    let i2 ← i + 1#usize
     let slots1 ← index_mut_back List.Nil
     HashMap.clear_loop T slots1 i2
   else Result.ok slots
@@ -80,8 +80,8 @@ divergent def HashMap.clear_loop
    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 0usize
-  Result.ok { self with num_entries := 0usize, slots := hm }
+  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 100:4-100:30 -/
@@ -129,7 +129,7 @@ def HashMap.insert_no_resize
   if inserted
   then
     do
-    let i1 ← self.num_entries + 1usize
+    let i1 ← self.num_entries + 1#usize
     let v ← index_mut_back l1
     Result.ok { self with num_entries := i1, slots := v }
   else do
@@ -169,7 +169,7 @@ divergent def HashMap.move_elements_loop
         (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
     let (ls, l1) := core.mem.replace (List T) l List.Nil
     let ntable1 ← HashMap.move_elements_from_list T ntable ls
-    let i2 ← i + 1usize
+    let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
     HashMap.move_elements_loop T ntable1 slots1 i2
   else Result.ok (ntable, slots)
@@ -189,15 +189,15 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
   let max_usize ← Scalar.cast .Usize core_u32_max
   let capacity := alloc.vec.Vec.len (List T) self.slots
-  let n1 ← max_usize / 2usize
+  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 * 2usize
+    let i3 ← capacity * 2#usize
     let ntable ← HashMap.new_with_capacity T i3 i i1
-    let p ← HashMap.move_elements T ntable self.slots 0usize
+    let p ← HashMap.move_elements T ntable self.slots 0#usize
     let (ntable1, _) := p
     Result.ok
       {
@@ -377,7 +377,7 @@ def HashMap.remove
     Result.ok (none, { self with slots := v })
   | some x1 =>
     do
-    let i1 ← self.num_entries - 1usize
+    let i1 ← self.num_entries - 1#usize
     let v ← index_mut_back l1
     Result.ok (some x1, { self with num_entries := i1, slots := v })
 
@@ -395,37 +395,37 @@ def insert_on_disk
 def test1 : Result Unit :=
   do
   let hm ← HashMap.new U64
-  let hm1 ← HashMap.insert U64 hm 0usize 42u64
-  let hm2 ← HashMap.insert U64 hm1 128usize 18u64
-  let hm3 ← HashMap.insert U64 hm2 1024usize 138u64
-  let hm4 ← HashMap.insert U64 hm3 1056usize 256u64
-  let i ← HashMap.get U64 hm4 128usize
-  if i = 18u64
+  let hm1 ← HashMap.insert U64 hm 0#usize 42#u64
+  let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64
+  let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64
+  let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64
+  let i ← HashMap.get U64 hm4 128#usize
+  if i = 18#u64
   then
     do
-    let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024usize
-    let hm5 ← get_mut_back 56u64
-    let i1 ← HashMap.get U64 hm5 1024usize
-    if i1 = 56u64
+    let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize
+    let hm5 ← get_mut_back 56#u64
+    let i1 ← HashMap.get U64 hm5 1024#usize
+    if i1 = 56#u64
     then
       do
-      let (x, hm6) ← HashMap.remove U64 hm5 1024usize
+      let (x, hm6) ← HashMap.remove U64 hm5 1024#usize
       match x with
       | none => Result.fail .panic
       | some x1 =>
-        if x1 = 56u64
+        if x1 = 56#u64
         then
           do
-          let i2 ← HashMap.get U64 hm6 0usize
-          if i2 = 42u64
+          let i2 ← HashMap.get U64 hm6 0#usize
+          if i2 = 42#u64
           then
             do
-            let i3 ← HashMap.get U64 hm6 128usize
-            if i3 = 18u64
+            let i3 ← HashMap.get U64 hm6 128#usize
+            if i3 = 18#u64
             then
               do
-              let i4 ← HashMap.get U64 hm6 1056usize
-              if i4 = 256u64
+              let i4 ← HashMap.get U64 hm6 1056#usize
+              if i4 = 256#u64
               then Result.ok ()
               else Result.fail .panic
             else Result.fail .panic
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 567d2b44..199605d5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -11,14 +11,14 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
   then do
        let s1 ← s + i
-       let i1 ← i + 1u32
+       let i1 ← i + 1#u32
        sum_loop max i1 s1
-  else s * 2u32
+  else s * 2#u32
 
 /- [loops::sum]:
    Source: 'tests/src/loops.rs', lines 8:0-8:27 -/
 def sum (max : U32) : Result U32 :=
-  sum_loop max 0u32 0u32
+  sum_loop max 0#u32 0#u32
 
 /- [loops::sum_with_mut_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 23:0-35:1 -/
@@ -28,14 +28,14 @@ divergent def sum_with_mut_borrows_loop
   then
     do
     let ms ← s + i
-    let mi ← i + 1u32
+    let mi ← i + 1#u32
     sum_with_mut_borrows_loop max mi ms
-  else s * 2u32
+  else s * 2#u32
 
 /- [loops::sum_with_mut_borrows]:
    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 0u32 0u32
+  sum_with_mut_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_with_shared_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 38:0-52:1 -/
@@ -44,15 +44,15 @@ divergent def sum_with_shared_borrows_loop
   if i < max
   then
     do
-    let i1 ← i + 1u32
+    let i1 ← i + 1#u32
     let s1 ← s + i1
     sum_with_shared_borrows_loop max i1 s1
-  else s * 2u32
+  else s * 2#u32
 
 /- [loops::sum_with_shared_borrows]:
    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 0u32 0u32
+  sum_with_shared_borrows_loop max 0#u32 0#u32
 
 /- [loops::sum_array]: loop 0:
    Source: 'tests/src/loops.rs', lines 54:0-62:1 -/
@@ -63,14 +63,14 @@ divergent def sum_array_loop
     do
     let i1 ← Array.index_usize U32 N a i
     let s1 ← s + i1
-    let i2 ← i + 1usize
+    let i2 ← i + 1#usize
     sum_array_loop N a i2 s1
   else Result.ok s
 
 /- [loops::sum_array]:
    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 0usize 0u32
+  sum_array_loop N a 0#usize 0#u32
 
 /- [loops::clear]: loop 0:
    Source: 'tests/src/loops.rs', lines 66:0-72:1 -/
@@ -83,15 +83,15 @@ divergent def clear_loop
     let (_, index_mut_back) ←
       alloc.vec.Vec.index_mut U32 Usize
         (core.slice.index.SliceIndexUsizeSliceTInst U32) v i
-    let i2 ← i + 1usize
-    let v1 ← index_mut_back 0u32
+    let i2 ← i + 1#usize
+    let v1 ← index_mut_back 0#u32
     clear_loop v1 i2
   else Result.ok v
 
 /- [loops::clear]:
    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 0usize
+  clear_loop v 0#usize
 
 /- [loops::List]
    Source: 'tests/src/loops.rs', lines 74:0-74:16 -/
@@ -119,13 +119,13 @@ divergent def list_nth_mut_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match ls with
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, back) ← list_nth_mut_loop_loop T tl i1
       let back1 :=
         fun ret => do
@@ -146,10 +146,10 @@ divergent def list_nth_shared_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then Result.ok x
     else do
-         let i1 ← i - 1u32
+         let i1 ← i - 1#u32
          list_nth_shared_loop_loop T tl i1
   | List.Nil => Result.fail .panic
 
@@ -189,7 +189,7 @@ def get_elem_mut
   do
   let (ls, index_mut_back) ←
     alloc.vec.Vec.index_mut (List Usize) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
+      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
   let (i, back) ← get_elem_mut_loop x ls
   let back1 := fun ret => do
                           let l ← back ret
@@ -213,7 +213,7 @@ def get_elem_shared
   do
   let ls ←
     alloc.vec.Vec.index (List Usize) Usize
-      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
+      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
   get_elem_shared_loop x ls
 
 /- [loops::id_mut]:
@@ -235,13 +235,13 @@ 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
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl
       let back1 :=
         fun ret => do
@@ -268,10 +268,10 @@ divergent def list_nth_shared_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then Result.ok x
     else do
-         let i1 ← i - 1u32
+         let i1 ← i - 1#u32
          list_nth_shared_loop_with_id_loop T i1 tl
   | List.Nil => Result.fail .panic
 
@@ -293,14 +293,14 @@ divergent def list_nth_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back'a := fun ret => Result.ok (List.Cons ret tl0)
         let back'b := fun ret => Result.ok (List.Cons ret tl1)
         Result.ok ((x0, x1), back'a, back'b)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
         let back'a1 :=
           fun ret => do
@@ -330,10 +330,10 @@ divergent def list_nth_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then Result.ok (x0, x1)
       else do
-           let i1 ← i - 1u32
+           let i1 ← i - 1#u32
            list_nth_shared_loop_pair_loop T tl0 tl1 i1
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
@@ -354,7 +354,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back :=
           fun ret =>
@@ -363,7 +363,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
         let back1 :=
           fun ret =>
@@ -390,11 +390,11 @@ divergent def list_nth_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then Result.ok (x0, x1)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         list_nth_shared_loop_pair_merge_loop T tl0 tl1 i1
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
@@ -415,13 +415,13 @@ divergent def list_nth_mut_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl0)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
         let back1 :=
           fun ret => do
@@ -449,13 +449,13 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl0)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
         let back1 :=
           fun ret => do
@@ -483,13 +483,13 @@ divergent def list_nth_shared_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl1)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
         let back1 :=
           fun ret => do
@@ -517,13 +517,13 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = 0u32
+      if i = 0#u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl1)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1u32
+        let i1 ← i - 1#u32
         let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
         let back1 :=
           fun ret => do
@@ -544,9 +544,9 @@ def list_nth_shared_mut_loop_pair_merge
 /- [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 349:0-353:1 -/
 divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
-  if i > 0u32
+  if i > 0#u32
   then do
-       let i1 ← i - 1u32
+       let i1 ← i - 1#u32
        ignore_input_mut_borrow_loop i1
   else Result.ok ()
 
@@ -560,9 +560,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
 /- [loops::incr_ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 357:0-362:1 -/
 divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
-  if i > 0u32
+  if i > 0#u32
   then do
-       let i1 ← i - 1u32
+       let i1 ← i - 1#u32
        incr_ignore_input_mut_borrow_loop i1
   else Result.ok ()
 
@@ -570,16 +570,16 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
    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 + 1u32
+  let a1 ← a + 1#u32
   let _ ← incr_ignore_input_mut_borrow_loop i
   Result.ok a1
 
 /- [loops::ignore_input_shared_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 366:0-370:1 -/
 divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
-  if i > 0u32
+  if i > 0#u32
   then do
-       let i1 ← i - 1u32
+       let i1 ← i - 1#u32
        ignore_input_shared_borrow_loop i1
   else Result.ok ()
 
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 34f899b1..3e3a558b 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
    Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
 def match_u32 (x : U32) : Result U32 :=
   match x with
-  | 0u32 => Result.ok 0u32
-  | 1u32 => Result.ok 1u32
-  | _ => Result.ok 2u32
+  | 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 01f6736c..f0438050 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -62,7 +62,7 @@ def cast_bool_to_bool (x : Bool) : Result Bool :=
    Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/
 def test2 : Result Unit :=
   do
-  let _ ← 23u32 + 44u32
+  let _ ← 23#u32 + 44#u32
   Result.ok ()
 
 /- Unit test for [no_nested_borrows::test2] -/
@@ -79,10 +79,10 @@ def get_max (x : U32) (y : U32) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/
 def test3 : Result Unit :=
   do
-  let x ← get_max 4u32 3u32
-  let y ← get_max 10u32 11u32
+  let x ← get_max 4#u32 3#u32
+  let y ← get_max 10#u32 11#u32
   let z ← x + y
-  if z = 15u32
+  if z = 15#u32
   then Result.ok ()
   else Result.fail .panic
 
@@ -93,8 +93,8 @@ def test3 : Result Unit :=
    Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/
 def test_neg1 : Result Unit :=
   do
-  let y ← -. 3i32
-  if y = (-3)i32
+  let y ← -. 3#i32
+  if y = (-3)#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -104,7 +104,7 @@ def test_neg1 : Result Unit :=
 /- [no_nested_borrows::refs_test1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/
 def refs_test1 : Result Unit :=
-  if 1i32 = 1i32
+  if 1#i32 = 1#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -114,12 +114,12 @@ def refs_test1 : Result Unit :=
 /- [no_nested_borrows::refs_test2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/
 def refs_test2 : Result Unit :=
-  if 2i32 = 2i32
+  if 2#i32 = 2#i32
   then
-    if 0i32 = 0i32
+    if 0#i32 = 0#i32
     then
-      if 2i32 = 2i32
-      then if 2i32 = 2i32
+      if 2#i32 = 2#i32
+      then if 2#i32 = 2#i32
            then Result.ok ()
            else Result.fail .panic
       else Result.fail .panic
@@ -141,10 +141,10 @@ def test_list1 : Result Unit :=
    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 0i32
-  let b ← deref_mut_back 1i32
+  let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32
+  let b ← deref_mut_back 1#i32
   let x ← alloc.boxed.Box.deref I32 b
-  if x = 1i32
+  if x = 1#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -174,8 +174,8 @@ def test_panic (b : Bool) : Result Unit :=
    Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/
 def test_copy_int : Result Unit :=
   do
-  let y ← copy_int 0i32
-  if 0i32 = y
+  let y ← copy_int 0#i32
+  if 0#i32 = y
   then Result.ok ()
   else Result.fail .panic
 
@@ -193,7 +193,7 @@ def is_cons (T : Type) (l : List T) : Result Bool :=
    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 0i32 List.Nil)
+  let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
   if b
   then Result.ok ()
   else Result.fail .panic
@@ -212,9 +212,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
    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 0i32 List.Nil)
+  let p ← split_list I32 (List.Cons 0#i32 List.Nil)
   let (hd, _) := p
-  if hd = 0i32
+  if hd = 0#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -237,14 +237,14 @@ def choose
    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 0i32 0i32
-  let z1 ← z + 1i32
-  if z1 = 1i32
+  let (z, choose_back) ← choose I32 true 0#i32 0#i32
+  let z1 ← z + 1#i32
+  if z1 = 1#i32
   then
     do
     let (x, y) ← choose_back z1
-    if x = 1i32
-    then if y = 0i32
+    if x = 1#i32
+    then if y = 0#i32
          then Result.ok ()
          else Result.fail .panic
     else Result.fail .panic
@@ -285,18 +285,18 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
   match l with
   | List.Cons _ l1 => do
                       let i ← list_length T l1
-                      1u32 + i
-  | List.Nil => Result.ok 0u32
+                      1#u32 + i
+  | List.Nil => Result.ok 0#u32
 
 /- [no_nested_borrows::list_nth_shared]:
    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 =>
-    if i = 0u32
+    if i = 0#u32
     then Result.ok x
     else do
-         let i1 ← i - 1u32
+         let i1 ← i - 1#u32
          list_nth_shared T tl i1
   | List.Nil => Result.fail .panic
 
@@ -306,13 +306,13 @@ divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
       let back :=
         fun ret =>
@@ -340,37 +340,37 @@ def list_rev (T : Type) (l : List T) : Result (List T) :=
    Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/
 def test_list_functions : Result Unit :=
   do
-  let l := List.Cons 2i32 List.Nil
-  let l1 := List.Cons 1i32 l
-  let i ← list_length I32 (List.Cons 0i32 l1)
-  if i = 3u32
+  let l := List.Cons 2#i32 List.Nil
+  let l1 := List.Cons 1#i32 l
+  let i ← list_length I32 (List.Cons 0#i32 l1)
+  if i = 3#u32
   then
     do
-    let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32
-    if i1 = 0i32
+    let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
+    if i1 = 0#i32
     then
       do
-      let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32
-      if i2 = 1i32
+      let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
+      if i2 = 1#i32
       then
         do
-        let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32
-        if i3 = 2i32
+        let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
+        if i3 = 2#i32
         then
           do
           let (_, list_nth_mut_back) ←
-            list_nth_mut I32 (List.Cons 0i32 l1) 1u32
-          let ls ← list_nth_mut_back 3i32
-          let i4 ← list_nth_shared I32 ls 0u32
-          if i4 = 0i32
+            list_nth_mut I32 (List.Cons 0#i32 l1) 1#u32
+          let ls ← list_nth_mut_back 3#i32
+          let i4 ← list_nth_shared I32 ls 0#u32
+          if i4 = 0#i32
           then
             do
-            let i5 ← list_nth_shared I32 ls 1u32
-            if i5 = 3i32
+            let i5 ← list_nth_shared I32 ls 1#u32
+            if i5 = 3#i32
             then
               do
-              let i6 ← list_nth_shared I32 ls 2u32
-              if i6 = 2i32
+              let i6 ← list_nth_shared I32 ls 2#u32
+              if i6 = 2#i32
               then Result.ok ()
               else Result.fail .panic
             else Result.fail .panic
@@ -425,17 +425,17 @@ structure StructWithTuple (T1 T2 : Type) where
 /- [no_nested_borrows::new_tuple1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
-  Result.ok { p := (1u32, 2u32) }
+  Result.ok { p := (1#u32, 2#u32) }
 
 /- [no_nested_borrows::new_tuple2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
-  Result.ok { p := (1i16, 2i16) }
+  Result.ok { p := (1#i16, 2#i16) }
 
 /- [no_nested_borrows::new_tuple3]:
    Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
-  Result.ok { p := (1u64, 2i64) }
+  Result.ok { p := (1#u64, 2#i64) }
 
 /- [no_nested_borrows::StructWithPair]
    Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/
@@ -445,7 +445,7 @@ structure StructWithPair (T1 T2 : Type) where
 /- [no_nested_borrows::new_pair1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
-  Result.ok { p := { x := 1u32, y := 2u32 } }
+  Result.ok { p := { x := 1#u32, y := 2#u32 } }
 
 /- [no_nested_borrows::test_constants]:
    Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/
@@ -453,21 +453,21 @@ def test_constants : Result Unit :=
   do
   let swt ← new_tuple1
   let (i, _) := swt.p
-  if i = 1u32
+  if i = 1#u32
   then
     do
     let swt1 ← new_tuple2
     let (i1, _) := swt1.p
-    if i1 = 1i16
+    if i1 = 1#i16
     then
       do
       let swt2 ← new_tuple3
       let (i2, _) := swt2.p
-      if i2 = 1u64
+      if i2 = 1#u64
       then
         do
         let swp ← new_pair1
-        if swp.p.x = 1u32
+        if swp.p.x = 1#u32
         then Result.ok ()
         else Result.fail .panic
       else Result.fail .panic
@@ -488,39 +488,39 @@ def test_weird_borrows1 : Result Unit :=
 /- [no_nested_borrows::test_mem_replace]:
    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 1u32
-  if y = 0u32
-  then Result.ok 2u32
+  let (y, _) := core.mem.replace U32 px 1#u32
+  if y = 0#u32
+  then Result.ok 2#u32
   else Result.fail .panic
 
 /- [no_nested_borrows::test_shared_borrow_bool1]:
    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 0u32
-  else Result.ok 1u32
+  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 427:0-427:40 -/
 def test_shared_borrow_bool2 : Result U32 :=
-  Result.ok 0u32
+  Result.ok 0#u32
 
 /- [no_nested_borrows::test_shared_borrow_enum1]:
    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 1u32
-  | List.Nil => Result.ok 0u32
+  | 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 454:0-454:40 -/
 def test_shared_borrow_enum2 : Result U32 :=
-  Result.ok 0u32
+  Result.ok 0#u32
 
 /- [no_nested_borrows::incr]:
    Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/
 def incr (x : U32) : Result U32 :=
-  x + 1u32
+  x + 1#u32
 
 /- [no_nested_borrows::call_incr]:
    Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/
@@ -531,7 +531,7 @@ def call_incr (x : U32) : Result U32 :=
    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 + 1u32
+  let x1 ← x + 1#u32
   Result.ok (x, x1)
 
 /- [no_nested_borrows::Tuple]
@@ -548,7 +548,7 @@ def read_tuple (x : (U32 × U32)) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/
 def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
   let (_, i) := x
-  Result.ok (1u32, i)
+  Result.ok (1#u32, i)
 
 /- [no_nested_borrows::read_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
@@ -560,7 +560,7 @@ def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
 def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
   let (_, i) := x
-  Result.ok (1u32, i)
+  Result.ok (1#u32, i)
 
 /- [no_nested_borrows::create_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 400406f1..03b96903 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -8,14 +8,14 @@ namespace paper
 /- [paper::ref_incr]:
    Source: 'tests/src/paper.rs', lines 7:0-7:28 -/
 def ref_incr (x : I32) : Result I32 :=
-  x + 1i32
+  x + 1#i32
 
 /- [paper::test_incr]:
    Source: 'tests/src/paper.rs', lines 11:0-11:18 -/
 def test_incr : Result Unit :=
   do
-  let x ← ref_incr 0i32
-  if x = 1i32
+  let x ← ref_incr 0#i32
+  if x = 1#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -38,14 +38,14 @@ def choose
    Source: 'tests/src/paper.rs', lines 26:0-26:20 -/
 def test_choose : Result Unit :=
   do
-  let (z, choose_back) ← choose I32 true 0i32 0i32
-  let z1 ← z + 1i32
-  if z1 = 1i32
+  let (z, choose_back) ← choose I32 true 0#i32 0#i32
+  let z1 ← z + 1#i32
+  if z1 = 1#i32
   then
     do
     let (x, y) ← choose_back z1
-    if x = 1i32
-    then if y = 0i32
+    if x = 1#i32
+    then if y = 0#i32
          then Result.ok ()
          else Result.fail .panic
     else Result.fail .panic
@@ -66,13 +66,13 @@ divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
   | List.Cons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
       let back :=
         fun ret =>
@@ -89,19 +89,19 @@ divergent def sum (l : List I32) : Result I32 :=
   | List.Cons x tl => do
                       let i ← sum tl
                       x + i
-  | List.Nil => Result.ok 0i32
+  | List.Nil => Result.ok 0#i32
 
 /- [paper::test_nth]:
    Source: 'tests/src/paper.rs', lines 71:0-71:17 -/
 def test_nth : Result Unit :=
   do
-  let l := List.Cons 3i32 List.Nil
-  let l1 := List.Cons 2i32 l
-  let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1i32 l1) 2u32
-  let x1 ← x + 1i32
+  let l := List.Cons 3#i32 List.Nil
+  let l1 := List.Cons 2#i32 l
+  let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32
+  let x1 ← x + 1#i32
   let l2 ← list_nth_mut_back x1
   let i ← sum l2
-  if i = 7i32
+  if i = 7#i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -114,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
   do
   let (px, py) := p
   let (pz, choose_back) ← choose U32 true px py
-  let pz1 ← pz + 1u32
+  let pz1 ← pz + 1#u32
   let (px1, _) ← choose_back pz1
   Result.ok px1
 
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 1cd8644b..0dd692fe 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -148,7 +148,7 @@ structure ToType (Self T : Type) where
 /- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
    Source: 'tests/src/traits.rs', lines 94:4-94:28 -/
 def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
-  Result.ok (self > 0u64)
+  Result.ok (self > 0#u64)
 
 /- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
    Source: 'tests/src/traits.rs', lines 93:0-93:25 -/
@@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where
    Source: 'tests/src/traits.rs', lines 140:12-140:34 -/
 def TestType.test.TestTraittraitsTestTypetestTestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
-  Result.ok (self > 1u64)
+  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 139:8-139:36 -/
@@ -217,8 +217,8 @@ def TestType.test
   (T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
   do
   let x1 ← ToU64Inst.to_u64 x
-  if x1 > 0u64
-  then TestType.test.TestTraittraitsTestTypetestTestType1.test 0u64
+  if x1 > 0#u64
+  then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
   else Result.ok false
 
 /- [traits::BoolWrapper]
@@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
 /- [traits::WithConstTy::LEN2]
    Source: 'tests/src/traits.rs', lines 165:4-165:21 -/
 def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
-  Result.ok 32usize
+  Result.ok 32#usize
 def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
   eval_global (WithConstTy.LEN2_default_body Self LEN)
 
@@ -259,19 +259,19 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
    Source: 'tests/src/traits.rs', lines 176:4-176:21 -/
-def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12usize
+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 181:4-181:39 -/
-def WithConstTyBool32.f (i : U64) (a : Array U8 32usize) : Result U64 :=
+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 175:0-175:29 -/
-def WithConstTyBool32 : WithConstTy Bool 32usize := {
+def WithConstTyBool32 : WithConstTy Bool 32#usize := {
   LEN1 := WithConstTyBool32.LEN1
-  LEN2 := WithConstTy.LEN2_default Bool 32usize
+  LEN2 := WithConstTy.LEN2_default Bool 32#usize
   V := U8
   W := U64
   W_clause_0 := ToU64U64
@@ -312,7 +312,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit :=
 /- [traits::test_where2]:
    Source: 'tests/src/traits.rs', lines 195:0-195:57 -/
 def test_where2
-  (T : Type) (WithConstTyT32Inst : WithConstTy T 32usize) (_x : U32) :
+  (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
   Result Unit
   :=
   Result.ok ()
@@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
    Source: 'tests/src/traits.rs', lines 320:4-320:20 -/
 def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
   : Result Usize :=
-  Result.ok 0usize
+  Result.ok 0#usize
 def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
   eval_global (TraittraitsWrapper.LEN_body T TraitInst)
 
@@ -522,7 +522,7 @@ inductive core.result.Result (T E : Type) :=
    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 0i32)
+  Result.ok (core.result.Result.Err 0#i32)
 def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
   eval_global (Foo.FOO_body T U TraitInst)