Make the `by inlit` implicit

11 files changed, 277 insertions, 331 deletions

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 37abdede..0506f4c0 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -356,8 +356,14 @@ def Scalar.ofIntCore {ty : ScalarTy} (x : Int)
   (hmin : Scalar.min ty ≤ x) (hmax : x ≤ Scalar.max ty) : Scalar ty :=
   { val := x, hmin := hmin, hmax := hmax }
 
+-- Tactic to prove that integers are in bounds
+-- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
+syntax "intlit" : tactic
+macro_rules
+  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices; decide)
+
 def Scalar.ofInt {ty : ScalarTy} (x : Int)
-  (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : Scalar ty :=
+  (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty := by intlit) : Scalar ty :=
   -- Remark: we initially wrote:
   --  let ⟨ hmin, hmax ⟩ := h
   --  Scalar.ofIntCore x hmin hmax
@@ -573,13 +579,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 
 def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val
 
--- Tactic to prove that integers are in bounds
--- TODO: use this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/instance.20with.20tactic.20autoparam
-syntax "intlit" : tactic
-
-macro_rules
-  | `(tactic| intlit) => `(tactic| apply Scalar.bound_suffices ; decide)
-
 -- -- We now define a type class that subsumes the various machine integer types, so
 -- -- as to write a concise definition for scalar_cast, rather than exhaustively
 -- -- enumerating all of the possible pairs. We remark that Rust has sane semantics
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 558a981d..b16f9639 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -820,7 +820,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
               F.pp_print_string fmt ")";
               F.pp_print_string fmt ")")
             else Z.pp_print fmt sv.value;
-            F.pp_print_string fmt " (by intlit))")
+            F.pp_print_string fmt ")")
     | Bool b ->
         let b =
           match !backend with
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index b0939155..142adf08 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -39,33 +39,33 @@ def betree.store_leaf_node
 /- [betree_main::betree::fresh_node_id]: forward function -/
 def betree.fresh_node_id (counter : U64) : Result U64 :=
   do
-    let _ ← counter + (U64.ofInt 1 (by intlit))
+    let _ ← counter + (U64.ofInt 1)
     Result.ret counter
 
 /- [betree_main::betree::fresh_node_id]: backward function 0 -/
 def betree.fresh_node_id_back (counter : U64) : Result U64 :=
-  counter + (U64.ofInt 1 (by intlit))
+  counter + (U64.ofInt 1)
 
 /- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
-  Result.ret { next_node_id := (U64.ofInt 0 (by intlit)) }
+  Result.ret { next_node_id := (U64.ofInt 0) }
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
 def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
   do
-    let _ ← self.next_node_id + (U64.ofInt 1 (by intlit))
+    let _ ← self.next_node_id + (U64.ofInt 1)
     Result.ret self.next_node_id
 
 /- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
 def betree.NodeIdCounter.fresh_id_back
   (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
   do
-    let i ← self.next_node_id + (U64.ofInt 1 (by intlit))
+    let i ← self.next_node_id + (U64.ofInt 1)
     Result.ret { next_node_id := i }
 
 /- [core::num::u64::{10}::MAX] -/
 def core_num_u64_max_body : Result U64 :=
-  Result.ret (U64.ofInt 18446744073709551615 (by intlit))
+  Result.ret (U64.ofInt 18446744073709551615)
 def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
 
 /- [betree_main::betree::upsert_update]: forward function -/
@@ -75,7 +75,7 @@ def betree.upsert_update
   | Option.none =>
     match st with
     | betree.UpsertFunState.Add v => Result.ret v
-    | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0 (by intlit))
+    | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0)
   | Option.some prev0 =>
     match st with
     | betree.UpsertFunState.Add v =>
@@ -87,7 +87,7 @@ def betree.upsert_update
     | betree.UpsertFunState.Sub v =>
       if prev0 >= v
       then prev0 - v
-      else Result.ret (U64.ofInt 0 (by intlit))
+      else Result.ret (U64.ofInt 0)
 
 /- [betree_main::betree::List::{1}::len]: forward function -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
@@ -95,21 +95,21 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   | betree.List.Cons t tl =>
     do
       let i ← betree.List.len T tl
-      (U64.ofInt 1 (by intlit)) + i
-  | betree.List.Nil => Result.ret (U64.ofInt 0 (by intlit))
+      (U64.ofInt 1) + i
+  | betree.List.Nil => Result.ret (U64.ofInt 0)
 
 /- [betree_main::betree::List::{1}::split_at]: forward function -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
   Result ((betree.List T) × (betree.List T))
   :=
-  if n = (U64.ofInt 0 (by intlit))
+  if n = (U64.ofInt 0)
   then Result.ret (betree.List.Nil, self)
   else
     match self with
     | betree.List.Cons hd tl =>
       do
-        let i ← n - (U64.ofInt 1 (by intlit))
+        let i ← n - (U64.ofInt 1)
         let p ← betree.List.split_at T tl i
         let (ls0, ls1) := p
         let l := ls0
@@ -740,7 +740,7 @@ mutual divergent def betree.Node.apply_messages
       let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2 (by intlit)) * params.split_size
+      let i ← (U64.ofInt 2) * params.split_size
       if len >= i
       then
         do
@@ -790,7 +790,7 @@ divergent def betree.Node.apply_messages_back
       let (st0, content) ← betree.load_leaf_node node.id st
       let content0 ← betree.Node.apply_messages_to_leaf content msgs
       let len ← betree.List.len (U64 × U64) content0
-      let i ← (U64.ofInt 2 (by intlit)) * params.split_size
+      let i ← (U64.ofInt 2) * params.split_size
       if len >= i
       then
         do
@@ -922,8 +922,7 @@ def betree.BeTree.new
         params :=
           { min_flush_size := min_flush_size, split_size := split_size },
         node_id_cnt := node_id_cnt0,
-        root :=
-          (betree.Node.Leaf { id := id, size := (U64.ofInt 0 (by intlit)) })
+        root := (betree.Node.Leaf { id := id, size := (U64.ofInt 0) })
       })
 
 /- [betree_main::betree::BeTree::{6}::apply]: forward function -/
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 8f22bfba..4a5a7b8f 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -5,12 +5,11 @@ open Primitives
 namespace constants
 
 /- [constants::X0] -/
-def x0_body : Result U32 := Result.ret (U32.ofInt 0 (by intlit))
+def x0_body : Result U32 := Result.ret (U32.ofInt 0)
 def x0_c : U32 := eval_global x0_body (by simp)
 
 /- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
-  Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
 def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
 
 /- [constants::X1] -/
@@ -18,15 +17,15 @@ def x1_body : Result U32 := Result.ret core_num_u32_max_c
 def x1_c : U32 := eval_global x1_body (by simp)
 
 /- [constants::X2] -/
-def x2_body : Result U32 := Result.ret (U32.ofInt 3 (by intlit))
+def x2_body : Result U32 := Result.ret (U32.ofInt 3)
 def x2_c : U32 := eval_global x2_body (by simp)
 
 /- [constants::incr]: forward function -/
 def incr (n : U32) : Result U32 :=
-  n + (U32.ofInt 1 (by intlit))
+  n + (U32.ofInt 1)
 
 /- [constants::X3] -/
-def x3_body : Result U32 := incr (U32.ofInt 32 (by intlit))
+def x3_body : Result U32 := incr (U32.ofInt 32)
 def x3_c : U32 := eval_global x3_body (by simp)
 
 /- [constants::mk_pair0]: forward function -/
@@ -43,23 +42,20 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
   Result.ret { x := x, y := y }
 
 /- [constants::P0] -/
-def p0_body : Result (U32 × U32) :=
-  mk_pair0 (U32.ofInt 0 (by intlit)) (U32.ofInt 1 (by intlit))
+def p0_body : Result (U32 × U32) := mk_pair0 (U32.ofInt 0) (U32.ofInt 1)
 def p0_c : (U32 × U32) := eval_global p0_body (by simp)
 
 /- [constants::P1] -/
-def p1_body : Result (Pair U32 U32) :=
-  mk_pair1 (U32.ofInt 0 (by intlit)) (U32.ofInt 1 (by intlit))
+def p1_body : Result (Pair U32 U32) := mk_pair1 (U32.ofInt 0) (U32.ofInt 1)
 def p1_c : Pair U32 U32 := eval_global p1_body (by simp)
 
 /- [constants::P2] -/
-def p2_body : Result (U32 × U32) :=
-  Result.ret ((U32.ofInt 0 (by intlit)), (U32.ofInt 1 (by intlit)))
+def p2_body : Result (U32 × U32) := Result.ret ((U32.ofInt 0), (U32.ofInt 1))
 def p2_c : (U32 × U32) := eval_global p2_body (by simp)
 
 /- [constants::P3] -/
 def p3_body : Result (Pair U32 U32) :=
-  Result.ret { x := (U32.ofInt 0 (by intlit)), y := (U32.ofInt 1 (by intlit)) }
+  Result.ret { x := (U32.ofInt 0), y := (U32.ofInt 1) }
 def p3_c : Pair U32 U32 := eval_global p3_body (by simp)
 
 /- [constants::Wrap] -/
@@ -71,7 +67,7 @@ def Wrap.new (T : Type) (val : T) : Result (Wrap T) :=
   Result.ret { val := val }
 
 /- [constants::Y] -/
-def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2 (by intlit))
+def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2)
 def y_c : Wrap I32 := eval_global y_body (by simp)
 
 /- [constants::unwrap_y]: forward function -/
@@ -83,7 +79,7 @@ def yval_body : Result I32 := unwrap_y
 def yval_c : I32 := eval_global yval_body (by simp)
 
 /- [constants::get_z1::Z1] -/
-def get_z1_z1_body : Result I32 := Result.ret (I32.ofInt 3 (by intlit))
+def get_z1_z1_body : Result I32 := Result.ret (I32.ofInt 3)
 def get_z1_z1_c : I32 := eval_global get_z1_z1_body (by simp)
 
 /- [constants::get_z1]: forward function -/
@@ -95,7 +91,7 @@ def add (a : I32) (b : I32) : Result I32 :=
   a + b
 
 /- [constants::Q1] -/
-def q1_body : Result I32 := Result.ret (I32.ofInt 5 (by intlit))
+def q1_body : Result I32 := Result.ret (I32.ofInt 5)
 def q1_c : I32 := eval_global q1_body (by simp)
 
 /- [constants::Q2] -/
@@ -103,7 +99,7 @@ def q2_body : Result I32 := Result.ret q1_c
 def q2_c : I32 := eval_global q2_body (by simp)
 
 /- [constants::Q3] -/
-def q3_body : Result I32 := add q2_c (I32.ofInt 3 (by intlit))
+def q3_body : Result I32 := add q2_c (I32.ofInt 3)
 def q3_c : I32 := eval_global q3_body (by simp)
 
 /- [constants::get_z2]: forward function -/
@@ -114,7 +110,7 @@ def get_z2 : Result I32 :=
     add q1_c i0
 
 /- [constants::S1] -/
-def s1_body : Result U32 := Result.ret (U32.ofInt 6 (by intlit))
+def s1_body : Result U32 := Result.ret (U32.ofInt 6)
 def s1_c : U32 := eval_global s1_body (by simp)
 
 /- [constants::S2] -/
@@ -126,8 +122,7 @@ def s3_body : Result (Pair U32 U32) := Result.ret p3_c
 def s3_c : Pair U32 U32 := eval_global s3_body (by simp)
 
 /- [constants::S4] -/
-def s4_body : Result (Pair U32 U32) :=
-  mk_pair1 (U32.ofInt 7 (by intlit)) (U32.ofInt 8 (by intlit))
+def s4_body : Result (Pair U32 U32) := mk_pair1 (U32.ofInt 7) (U32.ofInt 8)
 def s4_c : Pair U32 U32 := eval_global s4_body (by simp)
 
 end constants
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 122f94da..674aaebd 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -36,7 +36,7 @@ def test_new_non_zero_u32
 def test_vec : Result Unit :=
   do
     let v := Vec.new U32
-    let _ ← Vec.push U32 v (U32.ofInt 0 (by intlit))
+    let _ ← Vec.push U32 v (U32.ofInt 0)
     Result.ret ()
 
 /- Unit test for [external::test_vec] -/
@@ -74,14 +74,14 @@ def test_custom_swap_back
   (x : U32) (y : U32) (st : State) (st0 : State) :
   Result (State × (U32 × U32))
   :=
-  custom_swap_back U32 x y st (U32.ofInt 1 (by intlit)) st0
+  custom_swap_back U32 x y st (U32.ofInt 1) st0
 
 /- [external::test_swap_non_zero]: forward function -/
 def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
   do
-    let (st0, _) ← swap U32 x (U32.ofInt 0 (by intlit)) st
-    let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0 (by intlit)) st st0
-    if x0 = (U32.ofInt 0 (by intlit))
+    let (st0, _) ← swap U32 x (U32.ofInt 0) st
+    let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0) st st0
+    if x0 = (U32.ofInt 0)
     then Result.fail Error.panic
     else Result.ret (st1, x0)
 
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 5e11ffdd..870693b5 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -12,11 +12,11 @@ def hash_key (k : Usize) : Result Usize :=
 /- [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/
 divergent def HashMap.allocate_slots_loop
   (T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) :=
-  if n > (Usize.ofInt 0 (by intlit))
+  if n > (Usize.ofInt 0)
   then
     do
       let slots0 ← Vec.push (List T) slots List.Nil
-      let n0 ← n - (Usize.ofInt 1 (by intlit))
+      let n0 ← n - (Usize.ofInt 1)
       HashMap.allocate_slots_loop T slots0 n0
   else Result.ret slots
 
@@ -38,7 +38,7 @@ def HashMap.new_with_capacity
     let i0 ← i / max_load_divisor
     Result.ret
       {
-        num_entries := (Usize.ofInt 0 (by intlit)),
+        num_entries := (Usize.ofInt 0),
         max_load_factor := (max_load_dividend, max_load_divisor),
         max_load := i0,
         slots := slots
@@ -46,8 +46,7 @@ def HashMap.new_with_capacity
 
 /- [hashmap::HashMap::{0}::new]: forward function -/
 def HashMap.new (T : Type) : Result (HashMap T) :=
-  HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit))
-    (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit))
+  HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4) (Usize.ofInt 5)
 
 /- [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -57,7 +56,7 @@ divergent def HashMap.clear_loop
   if i < i0
   then
     do
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
       let slots0 ← Vec.index_mut_back (List T) slots i List.Nil
       HashMap.clear_loop T slots0 i1
   else Result.ret slots
@@ -66,9 +65,8 @@ divergent def HashMap.clear_loop
    (there is a single backward function, and the forward function returns ()) -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-    let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
-    Result.ret
-      { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
+    let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0)
+    Result.ret { self with num_entries := (Usize.ofInt 0), slots := v }
 
 /- [hashmap::HashMap::{0}::len]: forward function -/
 def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
@@ -123,7 +121,7 @@ def HashMap.insert_no_resize
     if inserted
     then
       do
-        let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries + (Usize.ofInt 1)
         let l0 ← HashMap.insert_in_list_back T key value l
         let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
         Result.ret { self with num_entries := i0, slots := v }
@@ -134,8 +132,7 @@ def HashMap.insert_no_resize
         Result.ret { self with slots := v }
 
 /- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
-  Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
 def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
 
 /- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
@@ -168,7 +165,7 @@ divergent def HashMap.move_elements_loop
       let l ← Vec.index_mut (List T) slots i
       let ls := mem.replace (List T) l List.Nil
       let ntable0 ← HashMap.move_elements_from_list T ntable ls
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
       let l0 := mem.replace_back (List T) l List.Nil
       let slots0 ← Vec.index_mut_back (List T) slots i l0
       HashMap.move_elements_loop T ntable0 slots0 i1
@@ -188,16 +185,16 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
     let max_usize ← Scalar.cast .Usize core_num_u32_max_c
     let capacity := Vec.len (List T) self.slots
-    let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
+    let n1 ← max_usize / (Usize.ofInt 2)
     let (i, i0) := self.max_load_factor
     let i1 ← n1 / i
     if capacity <= i1
     then
       do
-        let i2 ← capacity * (Usize.ofInt 2 (by intlit))
+        let i2 ← capacity * (Usize.ofInt 2)
         let ntable ← HashMap.new_with_capacity T i2 i i0
         let (ntable0, _) ←
-          HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit))
+          HashMap.move_elements T ntable self.slots (Usize.ofInt 0)
         Result.ret
           {
             ntable0
@@ -377,7 +374,7 @@ def HashMap.remove
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
-        let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
+        let _ ← self.num_entries - (Usize.ofInt 1)
         Result.ret (Option.some x0)
 
 /- [hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -397,7 +394,7 @@ def HashMap.remove_back
         Result.ret { self with slots := v }
     | Option.some x0 =>
       do
-        let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries - (Usize.ofInt 1)
         let l0 ← HashMap.remove_from_list_back T key l
         let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
         Result.ret { self with num_entries := i0, slots := v }
@@ -406,55 +403,43 @@ def HashMap.remove_back
 def test1 : Result Unit :=
   do
     let hm ← HashMap.new U64
-    let hm0 ←
-      HashMap.insert U64 hm (Usize.ofInt 0 (by intlit))
-        (U64.ofInt 42 (by intlit))
-    let hm1 ←
-      HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit))
-        (U64.ofInt 18 (by intlit))
-    let hm2 ←
-      HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit))
-        (U64.ofInt 138 (by intlit))
-    let hm3 ←
-      HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit))
-        (U64.ofInt 256 (by intlit))
-    let i ← HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit))
-    if not (i = (U64.ofInt 18 (by intlit)))
+    let hm0 ← HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42)
+    let hm1 ← HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18)
+    let hm2 ← HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138)
+    let hm3 ← HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256)
+    let i ← HashMap.get U64 hm3 (Usize.ofInt 128)
+    if not (i = (U64.ofInt 18))
     then Result.fail Error.panic
     else
       do
         let hm4 ←
-          HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit))
-            (U64.ofInt 56 (by intlit))
-        let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit))
-        if not (i0 = (U64.ofInt 56 (by intlit)))
+          HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024) (U64.ofInt 56)
+        let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024)
+        if not (i0 = (U64.ofInt 56))
         then Result.fail Error.panic
         else
           do
-            let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit))
+            let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024)
             match x with
             | Option.none => Result.fail Error.panic
             | Option.some x0 =>
-              if not (x0 = (U64.ofInt 56 (by intlit)))
+              if not (x0 = (U64.ofInt 56))
               then Result.fail Error.panic
               else
                 do
-                  let hm5 ←
-                    HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit))
-                  let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit))
-                  if not (i1 = (U64.ofInt 42 (by intlit)))
+                  let hm5 ← HashMap.remove_back U64 hm4 (Usize.ofInt 1024)
+                  let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0)
+                  if not (i1 = (U64.ofInt 42))
                   then Result.fail Error.panic
                   else
                     do
-                      let i2 ←
-                        HashMap.get U64 hm5 (Usize.ofInt 128 (by intlit))
-                      if not (i2 = (U64.ofInt 18 (by intlit)))
+                      let i2 ← HashMap.get U64 hm5 (Usize.ofInt 128)
+                      if not (i2 = (U64.ofInt 18))
                       then Result.fail Error.panic
                       else
                         do
-                          let i3 ←
-                            HashMap.get U64 hm5 (Usize.ofInt 1056 (by intlit))
-                          if not (i3 = (U64.ofInt 256 (by intlit)))
+                          let i3 ← HashMap.get U64 hm5 (Usize.ofInt 1056)
+                          if not (i3 = (U64.ofInt 256))
                           then Result.fail Error.panic
                           else Result.ret ()
 
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index e82cc9b2..610bae46 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -15,11 +15,11 @@ divergent def hashmap.HashMap.allocate_slots_loop
   (T : Type) (slots : Vec (hashmap.List T)) (n : Usize) :
   Result (Vec (hashmap.List T))
   :=
-  if n > (Usize.ofInt 0 (by intlit))
+  if n > (Usize.ofInt 0)
   then
     do
       let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil
-      let n0 ← n - (Usize.ofInt 1 (by intlit))
+      let n0 ← n - (Usize.ofInt 1)
       hashmap.HashMap.allocate_slots_loop T slots0 n0
   else Result.ret slots
 
@@ -43,7 +43,7 @@ def hashmap.HashMap.new_with_capacity
     let i0 ← i / max_load_divisor
     Result.ret
       {
-        num_entries := (Usize.ofInt 0 (by intlit)),
+        num_entries := (Usize.ofInt 0),
         max_load_factor := (max_load_dividend, max_load_divisor),
         max_load := i0,
         slots := slots
@@ -51,8 +51,8 @@ def hashmap.HashMap.new_with_capacity
 
 /- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/
 def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) :=
-  hashmap.HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit))
-    (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit))
+  hashmap.HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4)
+    (Usize.ofInt 5)
 
 /- [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -64,7 +64,7 @@ divergent def hashmap.HashMap.clear_loop
   if i < i0
   then
     do
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
       let slots0 ←
         Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil
       hashmap.HashMap.clear_loop T slots0 i1
@@ -75,10 +75,8 @@ divergent def hashmap.HashMap.clear_loop
 def hashmap.HashMap.clear
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
-    let v ←
-      hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
-    Result.ret
-      { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
+    let v ← hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0)
+    Result.ret { self with num_entries := (Usize.ofInt 0), slots := v }
 
 /- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/
 def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
@@ -138,7 +136,7 @@ def hashmap.HashMap.insert_no_resize
     if inserted
     then
       do
-        let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries + (Usize.ofInt 1)
         let l0 ← hashmap.HashMap.insert_in_list_back T key value l
         let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
         Result.ret { self with num_entries := i0, slots := v }
@@ -149,8 +147,7 @@ def hashmap.HashMap.insert_no_resize
         Result.ret { self with slots := v }
 
 /- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
-  Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
 def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
 
 /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
@@ -188,7 +185,7 @@ divergent def hashmap.HashMap.move_elements_loop
       let l ← Vec.index_mut (hashmap.List T) slots i
       let ls := mem.replace (hashmap.List T) l hashmap.List.Nil
       let ntable0 ← hashmap.HashMap.move_elements_from_list T ntable ls
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
       let l0 := mem.replace_back (hashmap.List T) l hashmap.List.Nil
       let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0
       hashmap.HashMap.move_elements_loop T ntable0 slots0 i1
@@ -210,17 +207,16 @@ def hashmap.HashMap.try_resize
   do
     let max_usize ← Scalar.cast .Usize core_num_u32_max_c
     let capacity := Vec.len (hashmap.List T) self.slots
-    let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
+    let n1 ← max_usize / (Usize.ofInt 2)
     let (i, i0) := self.max_load_factor
     let i1 ← n1 / i
     if capacity <= i1
     then
       do
-        let i2 ← capacity * (Usize.ofInt 2 (by intlit))
+        let i2 ← capacity * (Usize.ofInt 2)
         let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0
         let (ntable0, _) ←
-          hashmap.HashMap.move_elements T ntable self.slots
-            (Usize.ofInt 0 (by intlit))
+          hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0)
         Result.ret
           {
             ntable0
@@ -411,7 +407,7 @@ def hashmap.HashMap.remove
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
-        let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
+        let _ ← self.num_entries - (Usize.ofInt 1)
         Result.ret (Option.some x0)
 
 /- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -433,7 +429,7 @@ def hashmap.HashMap.remove_back
         Result.ret { self with slots := v }
     | Option.some x0 =>
       do
-        let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
+        let i0 ← self.num_entries - (Usize.ofInt 1)
         let l0 ← hashmap.HashMap.remove_from_list_back T key l
         let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
         Result.ret { self with num_entries := i0, slots := v }
@@ -442,60 +438,48 @@ def hashmap.HashMap.remove_back
 def hashmap.test1 : Result Unit :=
   do
     let hm ← hashmap.HashMap.new U64
-    let hm0 ←
-      hashmap.HashMap.insert U64 hm (Usize.ofInt 0 (by intlit))
-        (U64.ofInt 42 (by intlit))
-    let hm1 ←
-      hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit))
-        (U64.ofInt 18 (by intlit))
+    let hm0 ← hashmap.HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42)
+    let hm1 ← hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18)
     let hm2 ←
-      hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit))
-        (U64.ofInt 138 (by intlit))
+      hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138)
     let hm3 ←
-      hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit))
-        (U64.ofInt 256 (by intlit))
-    let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit))
-    if not (i = (U64.ofInt 18 (by intlit)))
+      hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256)
+    let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128)
+    if not (i = (U64.ofInt 18))
     then Result.fail Error.panic
     else
       do
         let hm4 ←
-          hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit))
-            (U64.ofInt 56 (by intlit))
-        let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit))
-        if not (i0 = (U64.ofInt 56 (by intlit)))
+          hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024)
+            (U64.ofInt 56)
+        let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024)
+        if not (i0 = (U64.ofInt 56))
         then Result.fail Error.panic
         else
           do
-            let x ←
-              hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit))
+            let x ← hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024)
             match x with
             | Option.none => Result.fail Error.panic
             | Option.some x0 =>
-              if not (x0 = (U64.ofInt 56 (by intlit)))
+              if not (x0 = (U64.ofInt 56))
               then Result.fail Error.panic
               else
                 do
                   let hm5 ←
-                    hashmap.HashMap.remove_back U64 hm4
-                      (Usize.ofInt 1024 (by intlit))
-                  let i1 ←
-                    hashmap.HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit))
-                  if not (i1 = (U64.ofInt 42 (by intlit)))
+                    hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024)
+                  let i1 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 0)
+                  if not (i1 = (U64.ofInt 42))
                   then Result.fail Error.panic
                   else
                     do
-                      let i2 ←
-                        hashmap.HashMap.get U64 hm5
-                          (Usize.ofInt 128 (by intlit))
-                      if not (i2 = (U64.ofInt 18 (by intlit)))
+                      let i2 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 128)
+                      if not (i2 = (U64.ofInt 18))
                       then Result.fail Error.panic
                       else
                         do
                           let i3 ←
-                            hashmap.HashMap.get U64 hm5
-                              (Usize.ofInt 1056 (by intlit))
-                          if not (i3 = (U64.ofInt 256 (by intlit)))
+                            hashmap.HashMap.get U64 hm5 (Usize.ofInt 1056)
+                          if not (i3 = (U64.ofInt 256))
                           then Result.fail Error.panic
                           else Result.ret ()
 
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 8cac7ac0..f7e6603d 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -8,16 +8,15 @@ namespace loops
 /- [loops::sum]: loop 0: forward function -/
 divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
   if i < max
-  then
-    do
-      let s0 ← s + i
-      let i0 ← i + (U32.ofInt 1 (by intlit))
-      sum_loop max i0 s0
-  else s * (U32.ofInt 2 (by intlit))
+  then do
+         let s0 ← s + i
+         let i0 ← i + (U32.ofInt 1)
+         sum_loop max i0 s0
+  else s * (U32.ofInt 2)
 
 /- [loops::sum]: forward function -/
 def sum (max : U32) : Result U32 :=
-  sum_loop max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
+  sum_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::sum_with_mut_borrows]: loop 0: forward function -/
 divergent def sum_with_mut_borrows_loop
@@ -26,14 +25,13 @@ divergent def sum_with_mut_borrows_loop
   then
     do
       let ms0 ← ms + mi
-      let mi0 ← mi + (U32.ofInt 1 (by intlit))
+      let mi0 ← mi + (U32.ofInt 1)
       sum_with_mut_borrows_loop max mi0 ms0
-  else ms * (U32.ofInt 2 (by intlit))
+  else ms * (U32.ofInt 2)
 
 /- [loops::sum_with_mut_borrows]: forward function -/
 def sum_with_mut_borrows (max : U32) : Result U32 :=
-  sum_with_mut_borrows_loop max (U32.ofInt 0 (by intlit))
-    (U32.ofInt 0 (by intlit))
+  sum_with_mut_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::sum_with_shared_borrows]: loop 0: forward function -/
 divergent def sum_with_shared_borrows_loop
@@ -41,15 +39,14 @@ divergent def sum_with_shared_borrows_loop
   if i < max
   then
     do
-      let i0 ← i + (U32.ofInt 1 (by intlit))
+      let i0 ← i + (U32.ofInt 1)
       let s0 ← s + i0
       sum_with_shared_borrows_loop max i0 s0
-  else s * (U32.ofInt 2 (by intlit))
+  else s * (U32.ofInt 2)
 
 /- [loops::sum_with_shared_borrows]: forward function -/
 def sum_with_shared_borrows (max : U32) : Result U32 :=
-  sum_with_shared_borrows_loop max (U32.ofInt 0 (by intlit))
-    (U32.ofInt 0 (by intlit))
+  sum_with_shared_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
 
 /- [loops::clear]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
@@ -58,15 +55,15 @@ divergent def clear_loop (v : Vec U32) (i : Usize) : Result (Vec U32) :=
   if i < i0
   then
     do
-      let i1 ← i + (Usize.ofInt 1 (by intlit))
-      let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit))
+      let i1 ← i + (Usize.ofInt 1)
+      let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0)
       clear_loop v0 i1
   else Result.ret v
 
 /- [loops::clear]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def clear (v : Vec U32) : Result (Vec U32) :=
-  clear_loop v (Usize.ofInt 0 (by intlit))
+  clear_loop v (Usize.ofInt 0)
 
 /- [loops::list_mem]: loop 0: forward function -/
 divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
@@ -85,12 +82,11 @@ divergent def list_nth_mut_loop_loop
   (T : Type) (ls : List T) (i : U32) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_loop T tl i0
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_mut_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop]: forward function -/
@@ -102,11 +98,11 @@ divergent def list_nth_mut_loop_loop_back
   (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -121,12 +117,11 @@ 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 = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_shared_loop_loop T tl i0
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_shared_loop_loop T tl i0
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_shared_loop]: forward function -/
@@ -144,7 +139,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
 /- [loops::get_elem_mut]: forward function -/
 def get_elem_mut (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
     get_elem_mut_loop x l
 
 /- [loops::get_elem_mut]: loop 0: backward function 0 -/
@@ -166,9 +161,9 @@ def get_elem_mut_back
   Result (Vec (List Usize))
   :=
   do
-    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
     let l0 ← get_elem_mut_loop_back x l ret0
-    Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
+    Vec.index_mut_back (List Usize) slots (Usize.ofInt 0) l0
 
 /- [loops::get_elem_shared]: loop 0: forward function -/
 divergent def get_elem_shared_loop
@@ -182,7 +177,7 @@ divergent def get_elem_shared_loop
 /- [loops::get_elem_shared]: forward function -/
 def get_elem_shared (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
   do
-    let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit))
+    let l ← Vec.index (List Usize) slots (Usize.ofInt 0)
     get_elem_shared_loop x l
 
 /- [loops::id_mut]: forward function -/
@@ -202,12 +197,11 @@ divergent def list_nth_mut_loop_with_id_loop
   (T : Type) (i : U32) (ls : List T) : Result T :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
-    else
-      do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
-        list_nth_mut_loop_with_id_loop T i0 tl
+    else do
+           let i0 ← i - (U32.ofInt 1)
+           list_nth_mut_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
 /- [loops::list_nth_mut_loop_with_id]: forward function -/
@@ -221,11 +215,11 @@ divergent def list_nth_mut_loop_with_id_loop_back
   (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
   match ls with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -243,11 +237,11 @@ 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 = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         list_nth_shared_loop_with_id_loop T i0 tl
   | List.Nil => Result.fail Error.panic
 
@@ -265,11 +259,11 @@ divergent def list_nth_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -288,11 +282,11 @@ divergent def list_nth_mut_loop_pair_loop_back'a
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
     | List.Nil => Result.fail Error.panic
@@ -314,11 +308,11 @@ divergent def list_nth_mut_loop_pair_loop_back'b
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
     | List.Nil => Result.fail Error.panic
@@ -338,11 +332,11 @@ divergent def list_nth_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -359,11 +353,11 @@ divergent def list_nth_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -382,12 +376,12 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then let (t, t0) := ret0
            Result.ret (List.Cons t tl0, List.Cons t0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let (tl00, tl10) ←
             list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
@@ -408,11 +402,11 @@ divergent def list_nth_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -429,11 +423,11 @@ divergent def list_nth_mut_shared_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -452,11 +446,11 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ←
             list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
@@ -477,11 +471,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -500,11 +494,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl0)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl00 ←
             list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x0 tl00)
@@ -525,11 +519,11 @@ divergent def list_nth_shared_mut_loop_pair_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -548,11 +542,11 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ←
             list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
@@ -573,11 +567,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (x0, x1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
     | List.Nil => Result.fail Error.panic
   | List.Nil => Result.fail Error.panic
@@ -596,11 +590,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
   | List.Cons x0 tl0 =>
     match ls1 with
     | List.Cons x1 tl1 =>
-      if i = (U32.ofInt 0 (by intlit))
+      if i = (U32.ofInt 0)
       then Result.ret (List.Cons ret0 tl1)
       else
         do
-          let i0 ← i - (U32.ofInt 1 (by intlit))
+          let i0 ← i - (U32.ofInt 1)
           let tl10 ←
             list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
           Result.ret (List.Cons x1 tl10)
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1c6421bb..bc707fd9 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -53,7 +53,7 @@ def div_test (x : U32) (y : U32) : Result U32 :=
 
 /- [no_nested_borrows::div_test1]: forward function -/
 def div_test1 (x : U32) : Result U32 :=
-  x / (U32.ofInt 2 (by intlit))
+  x / (U32.ofInt 2)
 
 /- [no_nested_borrows::rem_test]: forward function -/
 def rem_test (x : U32) (y : U32) : Result U32 :=
@@ -66,7 +66,7 @@ def cast_test (x : U32) : Result I32 :=
 /- [no_nested_borrows::test2]: forward function -/
 def test2 : Result Unit :=
   do
-    let _ ← (U32.ofInt 23 (by intlit)) + (U32.ofInt 44 (by intlit))
+    let _ ← (U32.ofInt 23) + (U32.ofInt 44)
     Result.ret ()
 
 /- Unit test for [no_nested_borrows::test2] -/
@@ -81,10 +81,10 @@ def get_max (x : U32) (y : U32) : Result U32 :=
 /- [no_nested_borrows::test3]: forward function -/
 def test3 : Result Unit :=
   do
-    let x ← get_max (U32.ofInt 4 (by intlit)) (U32.ofInt 3 (by intlit))
-    let y ← get_max (U32.ofInt 10 (by intlit)) (U32.ofInt 11 (by intlit))
+    let x ← get_max (U32.ofInt 4) (U32.ofInt 3)
+    let y ← get_max (U32.ofInt 10) (U32.ofInt 11)
     let z ← x + y
-    if not (z = (U32.ofInt 15 (by intlit)))
+    if not (z = (U32.ofInt 15))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -94,8 +94,8 @@ def test3 : Result Unit :=
 /- [no_nested_borrows::test_neg1]: forward function -/
 def test_neg1 : Result Unit :=
   do
-    let y ← - (I32.ofInt 3 (by intlit))
-    if not (y = (I32.ofInt (-(3:Int)) (by intlit)))
+    let y ← - (I32.ofInt 3)
+    if not (y = (I32.ofInt (-(3:Int))))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -104,7 +104,7 @@ def test_neg1 : Result Unit :=
 
 /- [no_nested_borrows::refs_test1]: forward function -/
 def refs_test1 : Result Unit :=
-  if not ((I32.ofInt 1 (by intlit)) = (I32.ofInt 1 (by intlit)))
+  if not ((I32.ofInt 1) = (I32.ofInt 1))
   then Result.fail Error.panic
   else Result.ret ()
 
@@ -113,16 +113,16 @@ def refs_test1 : Result Unit :=
 
 /- [no_nested_borrows::refs_test2]: forward function -/
 def refs_test2 : Result Unit :=
-  if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+  if not ((I32.ofInt 2) = (I32.ofInt 2))
   then Result.fail Error.panic
   else
-    if not ((I32.ofInt 0 (by intlit)) = (I32.ofInt 0 (by intlit)))
+    if not ((I32.ofInt 0) = (I32.ofInt 0))
     then Result.fail Error.panic
     else
-      if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+      if not ((I32.ofInt 2) = (I32.ofInt 2))
       then Result.fail Error.panic
       else
-        if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+        if not ((I32.ofInt 2) = (I32.ofInt 2))
         then Result.fail Error.panic
         else Result.ret ()
 
@@ -138,9 +138,9 @@ def test_list1 : Result Unit :=
 
 /- [no_nested_borrows::test_box1]: forward function -/
 def test_box1 : Result Unit :=
-  let b := (I32.ofInt 1 (by intlit))
+  let b := (I32.ofInt 1)
   let x := b
-  if not (x = (I32.ofInt 1 (by intlit)))
+  if not (x = (I32.ofInt 1))
   then Result.fail Error.panic
   else Result.ret ()
 
@@ -166,8 +166,8 @@ def test_panic (b : Bool) : Result Unit :=
 /- [no_nested_borrows::test_copy_int]: forward function -/
 def test_copy_int : Result Unit :=
   do
-    let y ← copy_int (I32.ofInt 0 (by intlit))
-    if not ((I32.ofInt 0 (by intlit)) = y)
+    let y ← copy_int (I32.ofInt 0)
+    if not ((I32.ofInt 0) = y)
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -184,7 +184,7 @@ def is_cons (T : Type) (l : List T) : Result Bool :=
 def test_is_cons : Result Unit :=
   do
     let l := List.Nil
-    let b ← is_cons I32 (List.Cons (I32.ofInt 0 (by intlit)) l)
+    let b ← is_cons I32 (List.Cons (I32.ofInt 0) l)
     if not b
     then Result.fail Error.panic
     else Result.ret ()
@@ -202,9 +202,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
 def test_split_list : Result Unit :=
   do
     let l := List.Nil
-    let p ← split_list I32 (List.Cons (I32.ofInt 0 (by intlit)) l)
+    let p ← split_list I32 (List.Cons (I32.ofInt 0) l)
     let (hd, _) := p
-    if not (hd = (I32.ofInt 0 (by intlit)))
+    if not (hd = (I32.ofInt 0))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -227,20 +227,17 @@ def choose_back
 /- [no_nested_borrows::choose_test]: forward function -/
 def choose_test : Result Unit :=
   do
-    let z ←
-      choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
-    let z0 ← z + (I32.ofInt 1 (by intlit))
-    if not (z0 = (I32.ofInt 1 (by intlit)))
+    let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0)
+    let z0 ← z + (I32.ofInt 1)
+    if not (z0 = (I32.ofInt 1))
     then Result.fail Error.panic
     else
       do
-        let (x, y) ←
-          choose_back I32 true (I32.ofInt 0 (by intlit))
-            (I32.ofInt 0 (by intlit)) z0
-        if not (x = (I32.ofInt 1 (by intlit)))
+        let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0
+        if not (x = (I32.ofInt 1))
         then Result.fail Error.panic
         else
-          if not (y = (I32.ofInt 0 (by intlit)))
+          if not (y = (I32.ofInt 0))
           then Result.fail Error.panic
           else Result.ret ()
 
@@ -268,20 +265,19 @@ end
 /- [no_nested_borrows::list_length]: forward function -/
 divergent def list_length (T : Type) (l : List T) : Result U32 :=
   match l with
-  | List.Cons t l1 =>
-    do
-      let i ← list_length T l1
-      (U32.ofInt 1 (by intlit)) + i
-  | List.Nil => Result.ret (U32.ofInt 0 (by intlit))
+  | List.Cons t l1 => do
+                        let i ← list_length T l1
+                        (U32.ofInt 1) + i
+  | List.Nil => Result.ret (U32.ofInt 0)
 
 /- [no_nested_borrows::list_nth_shared]: forward function -/
 divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
     else do
-           let i0 ← i - (U32.ofInt 1 (by intlit))
+           let i0 ← i - (U32.ofInt 1)
            list_nth_shared T tl i0
   | List.Nil => Result.fail Error.panic
 
@@ -289,10 +285,10 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
 divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
     else do
-           let i0 ← i - (U32.ofInt 1 (by intlit))
+           let i0 ← i - (U32.ofInt 1)
            list_nth_mut T tl i0
   | List.Nil => Result.fail Error.panic
 
@@ -301,11 +297,11 @@ divergent def list_nth_mut_back
   (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match l with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_back T tl i0 ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -327,52 +323,47 @@ def list_rev (T : Type) (l : List T) : Result (List T) :=
 def test_list_functions : Result Unit :=
   do
     let l := List.Nil
-    let l0 := List.Cons (I32.ofInt 2 (by intlit)) l
-    let l1 := List.Cons (I32.ofInt 1 (by intlit)) l0
-    let i ← list_length I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
-    if not (i = (U32.ofInt 3 (by intlit)))
+    let l0 := List.Cons (I32.ofInt 2) l
+    let l1 := List.Cons (I32.ofInt 1) l0
+    let i ← list_length I32 (List.Cons (I32.ofInt 0) l1)
+    if not (i = (U32.ofInt 3))
     then Result.fail Error.panic
     else
       do
         let i0 ←
-          list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
-            (U32.ofInt 0 (by intlit))
-        if not (i0 = (I32.ofInt 0 (by intlit)))
+          list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 0)
+        if not (i0 = (I32.ofInt 0))
         then Result.fail Error.panic
         else
           do
             let i1 ←
-              list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
-                (U32.ofInt 1 (by intlit))
-            if not (i1 = (I32.ofInt 1 (by intlit)))
+              list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 1)
+            if not (i1 = (I32.ofInt 1))
             then Result.fail Error.panic
             else
               do
                 let i2 ←
-                  list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
-                    (U32.ofInt 2 (by intlit))
-                if not (i2 = (I32.ofInt 2 (by intlit)))
+                  list_nth_shared I32 (List.Cons (I32.ofInt 0) l1)
+                    (U32.ofInt 2)
+                if not (i2 = (I32.ofInt 2))
                 then Result.fail Error.panic
                 else
                   do
                     let ls ←
-                      list_nth_mut_back I32 (List.Cons
-                        (I32.ofInt 0 (by intlit)) l1) (U32.ofInt 1 (by intlit))
-                        (I32.ofInt 3 (by intlit))
-                    let i3 ← list_nth_shared I32 ls (U32.ofInt 0 (by intlit))
-                    if not (i3 = (I32.ofInt 0 (by intlit)))
+                      list_nth_mut_back I32 (List.Cons (I32.ofInt 0) l1)
+                        (U32.ofInt 1) (I32.ofInt 3)
+                    let i3 ← list_nth_shared I32 ls (U32.ofInt 0)
+                    if not (i3 = (I32.ofInt 0))
                     then Result.fail Error.panic
                     else
                       do
-                        let i4 ←
-                          list_nth_shared I32 ls (U32.ofInt 1 (by intlit))
-                        if not (i4 = (I32.ofInt 3 (by intlit)))
+                        let i4 ← list_nth_shared I32 ls (U32.ofInt 1)
+                        if not (i4 = (I32.ofInt 3))
                         then Result.fail Error.panic
                         else
                           do
-                            let i5 ←
-                              list_nth_shared I32 ls (U32.ofInt 2 (by intlit))
-                            if not (i5 = (I32.ofInt 2 (by intlit)))
+                            let i5 ← list_nth_shared I32 ls (U32.ofInt 2)
+                            if not (i5 = (I32.ofInt 2))
                             then Result.fail Error.panic
                             else Result.ret ()
 
@@ -435,15 +426,15 @@ structure StructWithTuple (T1 T2 : Type) where
 
 /- [no_nested_borrows::new_tuple1]: forward function -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
-  Result.ret { p := ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit))) }
+  Result.ret { p := ((U32.ofInt 1), (U32.ofInt 2)) }
 
 /- [no_nested_borrows::new_tuple2]: forward function -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
-  Result.ret { p := ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit))) }
+  Result.ret { p := ((I16.ofInt 1), (I16.ofInt 2)) }
 
 /- [no_nested_borrows::new_tuple3]: forward function -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
-  Result.ret { p := ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit))) }
+  Result.ret { p := ((U64.ofInt 1), (I64.ofInt 2)) }
 
 /- [no_nested_borrows::StructWithPair] -/
 structure StructWithPair (T1 T2 : Type) where
@@ -451,32 +442,31 @@ structure StructWithPair (T1 T2 : Type) where
 
 /- [no_nested_borrows::new_pair1]: forward function -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
-  Result.ret
-  { p := { x := (U32.ofInt 1 (by intlit)), y := (U32.ofInt 2 (by intlit)) } }
+  Result.ret { p := { x := (U32.ofInt 1), y := (U32.ofInt 2) } }
 
 /- [no_nested_borrows::test_constants]: forward function -/
 def test_constants : Result Unit :=
   do
     let swt ← new_tuple1
     let (i, _) := swt.p
-    if not (i = (U32.ofInt 1 (by intlit)))
+    if not (i = (U32.ofInt 1))
     then Result.fail Error.panic
     else
       do
         let swt0 ← new_tuple2
         let (i0, _) := swt0.p
-        if not (i0 = (I16.ofInt 1 (by intlit)))
+        if not (i0 = (I16.ofInt 1))
         then Result.fail Error.panic
         else
           do
             let swt1 ← new_tuple3
             let (i1, _) := swt1.p
-            if not (i1 = (U64.ofInt 1 (by intlit)))
+            if not (i1 = (U64.ofInt 1))
             then Result.fail Error.panic
             else
               do
                 let swp ← new_pair1
-                if not (swp.p.x = (U32.ofInt 1 (by intlit)))
+                if not (swp.p.x = (U32.ofInt 1))
                 then Result.fail Error.panic
                 else Result.ret ()
 
@@ -493,29 +483,29 @@ def test_weird_borrows1 : Result Unit :=
 /- [no_nested_borrows::test_mem_replace]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def test_mem_replace (px : U32) : Result U32 :=
-  let y := mem.replace U32 px (U32.ofInt 1 (by intlit))
-  if not (y = (U32.ofInt 0 (by intlit)))
+  let y := mem.replace U32 px (U32.ofInt 1)
+  if not (y = (U32.ofInt 0))
   then Result.fail Error.panic
-  else Result.ret (U32.ofInt 2 (by intlit))
+  else Result.ret (U32.ofInt 2)
 
 /- [no_nested_borrows::test_shared_borrow_bool1]: forward function -/
 def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
   if b
-  then Result.ret (U32.ofInt 0 (by intlit))
-  else Result.ret (U32.ofInt 1 (by intlit))
+  then Result.ret (U32.ofInt 0)
+  else Result.ret (U32.ofInt 1)
 
 /- [no_nested_borrows::test_shared_borrow_bool2]: forward function -/
 def test_shared_borrow_bool2 : Result U32 :=
-  Result.ret (U32.ofInt 0 (by intlit))
+  Result.ret (U32.ofInt 0)
 
 /- [no_nested_borrows::test_shared_borrow_enum1]: forward function -/
 def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
   match l with
-  | List.Cons i l0 => Result.ret (U32.ofInt 1 (by intlit))
-  | List.Nil => Result.ret (U32.ofInt 0 (by intlit))
+  | List.Cons i l0 => Result.ret (U32.ofInt 1)
+  | List.Nil => Result.ret (U32.ofInt 0)
 
 /- [no_nested_borrows::test_shared_borrow_enum2]: forward function -/
 def test_shared_borrow_enum2 : Result U32 :=
-  Result.ret (U32.ofInt 0 (by intlit))
+  Result.ret (U32.ofInt 0)
 
 end no_nested_borrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index ade65656..cee7128a 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -7,13 +7,13 @@ namespace paper
 /- [paper::ref_incr]: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 def ref_incr (x : I32) : Result I32 :=
-  x + (I32.ofInt 1 (by intlit))
+  x + (I32.ofInt 1)
 
 /- [paper::test_incr]: forward function -/
 def test_incr : Result Unit :=
   do
-    let x ← ref_incr (I32.ofInt 0 (by intlit))
-    if not (x = (I32.ofInt 1 (by intlit)))
+    let x ← ref_incr (I32.ofInt 0)
+    if not (x = (I32.ofInt 1))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -36,20 +36,17 @@ def choose_back
 /- [paper::test_choose]: forward function -/
 def test_choose : Result Unit :=
   do
-    let z ←
-      choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
-    let z0 ← z + (I32.ofInt 1 (by intlit))
-    if not (z0 = (I32.ofInt 1 (by intlit)))
+    let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0)
+    let z0 ← z + (I32.ofInt 1)
+    if not (z0 = (I32.ofInt 1))
     then Result.fail Error.panic
     else
       do
-        let (x, y) ←
-          choose_back I32 true (I32.ofInt 0 (by intlit))
-            (I32.ofInt 0 (by intlit)) z0
-        if not (x = (I32.ofInt 1 (by intlit)))
+        let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0
+        if not (x = (I32.ofInt 1))
         then Result.fail Error.panic
         else
-          if not (y = (I32.ofInt 0 (by intlit)))
+          if not (y = (I32.ofInt 0))
           then Result.fail Error.panic
           else Result.ret ()
 
@@ -65,10 +62,10 @@ inductive List (T : Type) :=
 divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret x
     else do
-           let i0 ← i - (U32.ofInt 1 (by intlit))
+           let i0 ← i - (U32.ofInt 1)
            list_nth_mut T tl i0
   | List.Nil => Result.fail Error.panic
 
@@ -77,11 +74,11 @@ divergent def list_nth_mut_back
   (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
   match l with
   | List.Cons x tl =>
-    if i = (U32.ofInt 0 (by intlit))
+    if i = (U32.ofInt 0)
     then Result.ret (List.Cons ret0 tl)
     else
       do
-        let i0 ← i - (U32.ofInt 1 (by intlit))
+        let i0 ← i - (U32.ofInt 1)
         let tl0 ← list_nth_mut_back T tl i0 ret0
         Result.ret (List.Cons x tl0)
   | List.Nil => Result.fail Error.panic
@@ -92,23 +89,20 @@ divergent def sum (l : List I32) : Result I32 :=
   | List.Cons x tl => do
                         let i ← sum tl
                         x + i
-  | List.Nil => Result.ret (I32.ofInt 0 (by intlit))
+  | List.Nil => Result.ret (I32.ofInt 0)
 
 /- [paper::test_nth]: forward function -/
 def test_nth : Result Unit :=
   do
     let l := List.Nil
-    let l0 := List.Cons (I32.ofInt 3 (by intlit)) l
-    let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0
-    let x ←
-      list_nth_mut I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
-        (U32.ofInt 2 (by intlit))
-    let x0 ← x + (I32.ofInt 1 (by intlit))
+    let l0 := List.Cons (I32.ofInt 3) l
+    let l1 := List.Cons (I32.ofInt 2) l0
+    let x ← list_nth_mut I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2)
+    let x0 ← x + (I32.ofInt 1)
     let l2 ←
-      list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
-        (U32.ofInt 2 (by intlit)) x0
+      list_nth_mut_back I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2) x0
     let i ← sum l2
-    if not (i = (I32.ofInt 7 (by intlit)))
+    if not (i = (I32.ofInt 7))
     then Result.fail Error.panic
     else Result.ret ()
 
@@ -120,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
   do
     let (px, py) := p
     let pz ← choose U32 true px py
-    let pz0 ← pz + (U32.ofInt 1 (by intlit))
+    let pz0 ← pz + (U32.ofInt 1)
     let (px0, _) ← choose_back U32 true px py pz0
     Result.ret px0
 
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 75f7010a..8bbfb7cd 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -9,9 +9,15 @@
     "inputRev?": "v0.0.11"}},
   {"path": {"name": "Base", "dir": "./../../backends/lean"}},
   {"git":
+   {"url": "https://github.com/mhuisi/lean4-cli.git",
+    "subDir?": null,
+    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "name": "Cli",
+    "inputRev?": "nightly"}},
+  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "bb4fb766e41dd3a64197263ec132c7f9c4b50065",
+    "rev": "82fe7e902b01fe686b91c19550f1e228ad2dec1c",
     "name": "mathlib",
     "inputRev?": null}},
   {"git":