From 7763a8ef8d5190fad39e9e677c5f44c536973655 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:45:58 +0200
Subject: Add the Simp.Config to the simp wrappers

---
 backends/lean/Base/Arith/Int.lean         |  6 ++--
 backends/lean/Base/Arith/Scalar.lean      | 47 +++++++++++++++----------------
 backends/lean/Base/Progress/Progress.lean |  4 +--
 backends/lean/Base/Utils.lean             | 16 +++++------
 4 files changed, 36 insertions(+), 37 deletions(-)

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 4a3db5f8..59cdca25 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -180,7 +180,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    Utils.simpAt true [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
+    Utils.simpAt true {} [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
     -- Return the new value
     pure nval
 
@@ -214,7 +214,7 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
   extraPreprocess
   -- Reduce all the terms in the goal - note that the extra preprocessing step
   -- might have proven the goal, hence the `Tactic.allGoals`
-  Tactic.allGoals do tryTac (dsimpAt false [] [] [] Tactic.Location.wildcard)
+  Tactic.allGoals do tryTac (dsimpAt false {} [] [] [] Tactic.Location.wildcard)
 
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess (do pure ())
@@ -231,7 +231,7 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
   -- More preprocessing
-  Tactic.allGoals (Utils.tryTac (Utils.simpAt true [] [``nat_zero_eq_int_zero] [] .wildcard))
+  Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} [] [``nat_zero_eq_int_zero] [] .wildcard))
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 86b2e216..c2e4e24e 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -8,30 +8,29 @@ open Lean Lean.Elab Lean.Meta
 open Primitives
 
 def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
-   Tactic.withMainContext do
-   -- Inroduce the bounds for the isize/usize types
-   let add (e : Expr) : Tactic.TacticM Unit := do
-     let ty ← inferType e
-     let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
-   add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
-   add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
-   add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-   -- Reveal the concrete bounds, simplify calls to [ofInt]
-   Utils.simpAt true
-                -- Unfoldings
-                [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
-                 ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
-                 ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
-                 ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
-                 ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
-                 ``Usize.min
-                 ]
-                 -- Simp lemmas
-                 [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val,
-                  ``Scalar.lt_equiv, ``Scalar.le_equiv, ``Scalar.eq_equiv]
-                 -- Hypotheses
-                 [] .wildcard
-   
+  Tactic.withMainContext do
+  -- Inroduce the bounds for the isize/usize types
+  let add (e : Expr) : Tactic.TacticM Unit := do
+    let ty ← inferType e
+    let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false)
+  add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
+  add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
+  add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
+  -- Reveal the concrete bounds, simplify calls to [ofInt]
+  Utils.simpAt true {}
+               -- Unfoldings
+               [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
+                ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
+                ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
+                ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
+                ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
+                ``Usize.min
+                ]
+                -- Simp lemmas
+                [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val,
+                 ``Scalar.lt_equiv, ``Scalar.le_equiv, ``Scalar.eq_equiv]
+                -- Hypotheses
+                [] .wildcard
 
 elab "scalar_tac_preprocess" : tactic =>
   intTacPreprocess scalarTacExtraPreprocess
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index f2a56e50..39a48044 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -135,7 +135,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     Tactic.focus do
     let _ ←
       tryTac
-        (simpAt true []
+        (simpAt true {} []
                [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
                [hEq.fvarId!] (.targets #[] true))
     -- It may happen that at this point the goal is already solved (though this is rare)
@@ -144,7 +144,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     else
        trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
        -- TODO: remove this (some types get unfolded too much: we "fold" them back)
-       let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
+       let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep)
        trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
        -- Clear the equality, unless the user requests not to do so
        let mgoal ← do
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 7ae5a832..6ee854cc 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -664,7 +664,7 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
    Something very annoying is that there is no function which allows to
    initialize a simp context without doing an elaboration - as a consequence
    we write our own here. -/
-def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
   Tactic.TacticM Simp.Context := do
   -- Initialize either with the builtin simp theorems or with all the simp theorems
   let simpThms ←
@@ -693,7 +693,7 @@ def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (
         throwError "Not a proposition: {thmName}"
       ) simpThms
   let congrTheorems ← getSimpCongrTheorems
-  pure { simpTheorems := #[simpThms], congrTheorems }
+  pure { config, simpTheorems := #[simpThms], congrTheorems }
 
 inductive Location where
   /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/
@@ -731,28 +731,28 @@ where
     return usedSimps
 
 /- Call the simp tactic. -/
-def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+def simpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
   (loc : Location) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse
+  let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
   -- Apply the simplifier
   let _ ← customSimpLocation ctx (discharge? := .none) loc
 
 /- Call the dsimp tactic. -/
-def dsimpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+def dsimpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
   (loc : Tactic.Location) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse
+  let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse
   -- Apply the simplifier
   dsimpLocation ctx loc
 
 -- Call the simpAll tactic
-def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+def simpAll (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
   Tactic.TacticM Unit := do
   -- Initialize the simp context
-  let ctx ← mkSimpCtx false declsToUnfold thms hypsToUse
+  let ctx ← mkSimpCtx false config declsToUnfold thms hypsToUse
   -- Apply the simplifier
   let _ ← Lean.Meta.simpAll (← getMainGoal) ctx
 
-- 
cgit v1.2.3


From 191927e2fd21cf94501ac4f4968b09d110043d33 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:46:21 +0200
Subject: Add wrappers around the rewriter

---
 backends/lean/Base/Utils.lean | 61 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 61 insertions(+)

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 6ee854cc..4be46400 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -756,4 +756,65 @@ def simpAll (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name
   -- Apply the simplifier
   let _ ← Lean.Meta.simpAll (← getMainGoal) ctx
 
+/- Adapted from Elab.Tactic.Rewrite -/
+def rewriteTarget (eqThm : Expr) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
+  Term.withSynthesize <| withMainContext do
+    let r ← (← getMainGoal).rewrite (← getMainTarget) eqThm symm (config := config)
+    let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
+    replaceMainGoal (mvarId' :: r.mvarIds)
+
+/- Adapted from Elab.Tactic.Rewrite -/
+def rewriteLocalDecl (eqThm : Expr) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) :
+    TacticM Unit := withMainContext do
+  -- Note: we cannot execute `replaceLocalDecl` inside `Term.withSynthesize`.
+  -- See issues #2711 and #2727.
+  let rwResult ← Term.withSynthesize <| withMainContext do
+    let localDecl ← fvarId.getDecl
+    (← getMainGoal).rewrite localDecl.type eqThm symm (config := config)
+  let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
+  replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
+
+/- Adapted from Elab.Tactic.Rewrite -/
+def rewriteWithThms
+  (thms : List (Bool × Expr))
+  (rewrite : (symm : Bool) → (thm : Expr) → TacticM Unit)
+  : TacticM Unit := do
+  let rec go thms :=
+    match thms with
+    | [] => throwError "Failed to rewrite with any theorem"
+    | (symm, eqThm)::thms =>
+      rewrite symm eqThm <|> go thms
+  go thms
+
+/- Adapted from Elab.Tactic.Rewrite -/
+def evalRewriteSeqAux (cfg : Rewrite.Config) (thms : List (Bool × Expr)) (loc : Tactic.Location) : TacticM Unit :=
+  rewriteWithThms thms fun symm term => do
+    withLocation loc
+      (rewriteLocalDecl term symm · cfg)
+      (rewriteTarget term symm cfg)
+      (throwTacticEx `rewrite · "did not find instance of the pattern in the current goal")
+
+/-- `rpt`: if `true`, repeatedly rewrite -/
+def rewriteAt (cfg : Rewrite.Config) (rpt : Bool)
+  (thms : List (Bool × Name)) (loc : Tactic.Location) : TacticM Unit := do
+  -- Lookup the theorems
+  let lookupThm (x : Bool × Name) : TacticM (List (Bool × Expr)) := do
+    let thName := x.snd
+    let lookupOne (thName : Name) : TacticM (Bool × Expr) := do
+      -- Lookup the theorem and introduce fresh meta-variables for the universes
+      let th ← mkConstWithFreshMVarLevels thName
+      pure (x.fst, th)
+    match ← getEqnsFor? thName (nonRec := true) with
+    | some eqThms => do
+      eqThms.data.mapM lookupOne
+    | none => do
+      pure [← lookupOne thName]
+  let thms ← List.mapM lookupThm thms
+  let thms := thms.flatten
+  -- Rewrite
+  if rpt then
+    Utils.repeatTac (evalRewriteSeqAux cfg thms loc)
+  else
+    evalRewriteSeqAux cfg thms loc
+
 end Utils
-- 
cgit v1.2.3


From f5deac2b0f42e2a87fc26da50c902729e0ed1039 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:46:38 +0200
Subject: Slightly simplify the progress tactic

---
 backends/lean/Base/Progress/Progress.lean | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 39a48044..03d464d7 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -58,17 +58,13 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
      We also make sure that all the meta variables which appear in the
      function arguments have been instantiated
    -/
-  let env ← getEnv
   let thTy ← do
     match th with
     | .Theorem thName =>
-      let thDecl := env.constants.find! thName
-      -- We have to introduce fresh meta-variables for the universes already
-      let ul : List (Name × Level) ←
-        thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar))
-      let ulMap : HashMap Name Level := HashMap.ofList ul
-      let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x)
-      pure thTy
+      -- Lookup the theorem and introduce fresh meta-variables for the universes
+      let th ← mkConstWithFreshMVarLevels thName
+      -- Retrieve the type
+      inferType th
     | .Local asmDecl => pure asmDecl.type
   trace[Progress] "Looked up theorem/assumption type: {thTy}"
   -- TODO: the tactic fails if we uncomment withNewMCtxDepth
-- 
cgit v1.2.3


From 1018aa1af83e639a6b41b5650bf3b717e7f8de68 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:46:52 +0200
Subject: Deactivate the coercion from Nat to Scalar

---
 backends/lean/Base/Arith/Scalar.lean      | 10 ++++++++++
 backends/lean/Base/Primitives/Scalar.lean |  7 +++++++
 2 files changed, 17 insertions(+)

diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index c2e4e24e..8793713b 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -80,4 +80,14 @@ example (x : Int) (h0 : 0 ≤ x) (h1 : x ≤ U32.max) :
 example (x : U32) (h0 : ¬ x = U32.ofInt 0) : 0 < x.val := by
   scalar_tac
 
+/- See this: https://aeneas-verif.zulipchat.com/#narrow/stream/349819-general/topic/U64.20trouble/near/444049757
+
+   We solved it by removing the instance `OfNat` for `Scalar`.
+   Note however that we could also solve it with a simplification lemma.
+   However, after testing, we noticed we could only apply such a lemma with
+   the rewriting tactic (not the simplifier), probably because of the use
+   of typeclasses. -/
+example {u: U64} (h1: (u : Int) < 2): (u : Int) = 0 ∨ (u : Int) = 1 := by
+  scalar_tac
+
 end Arith
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 8fb067e1..157ade2c 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -351,10 +351,17 @@ instance [Decide (Scalar.cMin ty ≤ v ∧ v ≤ Scalar.cMax ty)] : InBounds ty
 @[simp] abbrev Scalar.check_bounds (ty : ScalarTy) (x : Int) : Bool :=
   (Scalar.cMin ty ≤ x || Scalar.min ty ≤ x) ∧ (x ≤ Scalar.cMax ty || x ≤ Scalar.max ty)
 
+/- Discussion:
+   This coercion can be slightly annoying at times, because if we write
+   something like `u = 3` (where `u` is, for instance, as `U32`), then instead of
+   coercing `u` to `Int`, Lean will lift `3` to `U32`).
+   For now we deactivate it.
+
 -- TODO(raitobezarius): the inbounds constraint is a bit ugly as we can pretty trivially
 -- discharge the lhs on ≥ 0.
 instance {ty: ScalarTy} [InBounds ty (Int.ofNat n)]: OfNat (Scalar ty) (n: ℕ) where
   ofNat := Scalar.ofInt n
+-/
 
 theorem Scalar.check_bounds_imp_in_bounds {ty : ScalarTy} {x : Int}
   (h: Scalar.check_bounds ty x) :
-- 
cgit v1.2.3


From c8272aeea205ca9cb36e22757473ca2a931a4933 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:52:34 +0200
Subject: Update the scalar notation for the Lean backend

---
 backends/lean/Base/Primitives/Scalar.lean | 50 +++++++++++++++----------------
 compiler/ExtractTypes.ml                  |  2 +-
 2 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 157ade2c..5f14a14f 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -313,13 +313,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
 /- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `#u32` (which
+   This is particularly useful once we introduce notations like `u32` (which
    desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
    Example:
    ```
    match x with
-   | 0#u32 => ...
-   | 1#u32 => ...
+   | 0u32 => ...
+   | 1u32 => ...
    | ...
    ```
  -/
@@ -328,7 +328,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   { val := x, hmin := h.left, hmax := h.right }
 
 -- The definitions below are used later to introduce nice syntax for constants,
--- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
+-- like `1u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
 
 class InBounds (ty : ScalarTy) (x : Int) :=
   hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
@@ -1281,38 +1281,38 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 @[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
 @[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
 
-postfix:max "#isize" => Isize.ofInt
-postfix:max "#i8"    => I8.ofInt
-postfix:max "#i16"   => I16.ofInt
-postfix:max "#i32"   => I32.ofInt
-postfix:max "#i64"   => I64.ofInt
-postfix:max "#i128"  => I128.ofInt
-postfix:max "#usize" => Usize.ofInt
-postfix:max "#u8"    => U8.ofInt
-postfix:max "#u16"   => U16.ofInt
-postfix:max "#u32"   => U32.ofInt
-postfix:max "#u64"   => U64.ofInt
-postfix:max "#u128"  => U128.ofInt
+postfix:max "isize" => Isize.ofInt
+postfix:max "i8"    => I8.ofInt
+postfix:max "i16"   => I16.ofInt
+postfix:max "i32"   => I32.ofInt
+postfix:max "i64"   => I64.ofInt
+postfix:max "i128"  => I128.ofInt
+postfix:max "usize" => Usize.ofInt
+postfix:max "u8"    => U8.ofInt
+postfix:max "u16"   => U16.ofInt
+postfix:max "u32"   => U32.ofInt
+postfix:max "u64"   => U64.ofInt
+postfix:max "u128"  => U128.ofInt
 
 /- Testing the notations -/
-example := 0#u32
-example := 1#u32
-example := 1#i32
-example := 0#isize
-example := (-1)#isize
+example := 0u32
+example := 1u32
+example := 1i32
+example := 0isize
+example := (-1)isize
 example (x : U32) : Bool :=
   match x with
-  | 0#u32 => true
+  | 0u32 => true
   | _ => false
 
 example (x : U32) : Bool :=
   match x with
-  | 1#u32 => true
+  | 1u32 => true
   | _ => false
 
 example (x : I32) : Bool :=
   match x with
-  | (-1)#i32 => true
+  | (-1)i32 => true
   | _ => false
 
 -- Notation for pattern matching
@@ -1334,7 +1334,7 @@ example {ty} (x : Scalar ty) : Bool :=
   | _ => false
 
 -- Testing the notations
-example : Result Usize := 0#usize + 1#usize
+example : Result Usize := 0usize + 1usize
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 15e75da2..5446f912 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
               let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt ("#" ^ iname)
+              F.pp_print_string fmt iname
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
-- 
cgit v1.2.3


From cd5542fc82edee11181a43e3a342a2567c929e7e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:53:12 +0200
Subject: Regenerate the tests

---
 tests/lean/Arrays.lean          | 225 ++++++++++++++++++++--------------------
 tests/lean/Betree/Funs.lean     |  22 ++--
 tests/lean/Bitwise.lean         |   8 +-
 tests/lean/Constants.lean       |  28 ++---
 tests/lean/Demo/Demo.lean       |  28 ++---
 tests/lean/External/Funs.lean   |   2 +-
 tests/lean/Hashmap/Funs.lean    |  62 +++++------
 tests/lean/Loops.lean           |  94 ++++++++---------
 tests/lean/Matches.lean         |   6 +-
 tests/lean/NoNestedBorrows.lean | 138 ++++++++++++------------
 tests/lean/Paper.lean           |  34 +++---
 tests/lean/Traits.lean          |  24 ++---
 12 files changed, 333 insertions(+), 338 deletions(-)

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 9748919e..70b4a26b 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 + 1#u32
+  x + 1u32
 
 /- [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 32#usize) : Result (Slice T) :=
-  Array.to_slice T 32#usize s
+  (T : Type) (s : Array T 32usize) : Result (Slice T) :=
+  Array.to_slice T 32usize 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 32#usize) :
-  Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
+  (T : Type) (s : Array T 32usize) :
+  Result ((Slice T) × (Slice T → Result (Array T 32usize)))
   :=
-  Array.to_slice_mut T 32#usize s
+  Array.to_slice_mut T 32usize s
 
 /- [arrays::array_len]:
    Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/
-def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
+def array_len (T : Type) (s : Array T 32usize) : Result Usize :=
   do
-  let s1 ← Array.to_slice T 32#usize s
+  let s1 ← Array.to_slice T 32usize 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 32#usize) : Result Usize :=
+def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize :=
   do
-  let s1 ← Array.to_slice T 32#usize s
+  let s1 ← Array.to_slice T 32usize 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 32#usize) (i : Usize) : Result T :=
-  Array.index_usize T 32#usize s i
+  (T : Type) (s : Array T 32usize) (i : Usize) : Result T :=
+  Array.index_usize T 32usize s i
 
 /- [arrays::index_array_u32]:
    Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/
-def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 :=
-  Array.index_usize U32 32#usize s i
+def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 :=
+  Array.index_usize U32 32usize s i
 
 /- [arrays::index_array_copy]:
    Source: 'tests/src/arrays.rs', lines 51:0-51:45 -/
-def index_array_copy (x : Array U32 32#usize) : Result U32 :=
-  Array.index_usize U32 32#usize x 0#usize
+def index_array_copy (x : Array U32 32usize) : Result U32 :=
+  Array.index_usize U32 32usize x 0usize
 
 /- [arrays::index_mut_array]:
    Source: 'tests/src/arrays.rs', lines 55:0-55:62 -/
 def index_mut_array
-  (T : Type) (s : Array T 32#usize) (i : Usize) :
-  Result (T × (T → Result (Array T 32#usize)))
+  (T : Type) (s : Array T 32usize) (i : Usize) :
+  Result (T × (T → Result (Array T 32usize)))
   :=
-  Array.index_mut_usize T 32#usize s i
+  Array.index_mut_usize T 32usize 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 32#usize) : Result (Slice U32) :=
-  Array.to_slice U32 32#usize x
+def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) :=
+  Array.to_slice U32 32usize x
 
 /- [arrays::array_to_slice_mut_]:
    Source: 'tests/src/arrays.rs', lines 79:0-79:59 -/
 def array_to_slice_mut_
-  (x : Array U32 32#usize) :
-  Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
+  (x : Array U32 32usize) :
+  Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
   :=
-  Array.to_slice_mut U32 32#usize x
+  Array.to_slice_mut U32 32usize x
 
 /- [arrays::array_subslice_shared_]:
    Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/
 def array_subslice_shared_
-  (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
-  core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
+  (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
     (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 32#usize) (y : Usize) (z : Usize) :
-  Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
+  (x : Array U32 32usize) (y : Usize) (z : Usize) :
+  Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
   :=
   do
   let (s, index_mut_back) ←
-    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize
+    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize
       (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 0#usize
+  Slice.index_usize T s 0usize
 
 /- [arrays::index_array_0]:
    Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/
-def index_array_0 (T : Type) (s : Array T 32#usize) : Result T :=
-  Array.index_usize T 32#usize s 0#usize
+def index_array_0 (T : Type) (s : Array T 32usize) : Result T :=
+  Array.index_usize T 32usize s 0usize
 
 /- [arrays::index_index_array]:
    Source: 'tests/src/arrays.rs', lines 106:0-106:71 -/
 def index_index_array
-  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
+  (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
   Result U32
   :=
   do
-  let a ← Array.index_usize (Array U32 32#usize) 32#usize s i
-  Array.index_usize U32 32#usize a j
+  let a ← Array.index_usize (Array U32 32usize) 32usize s i
+  Array.index_usize U32 32usize a j
 
 /- [arrays::update_update_array]:
    Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/
 def update_update_array
-  (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
+  (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
   Result Unit
   :=
   do
   let (a, index_mut_back) ←
-    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
+    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
   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 32#usize) : Result Unit :=
+def array_local_deep_copy (x : Array U32 32usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_array]:
    Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/
-def take_array (a : Array U32 2#usize) : Result Unit :=
+def take_array (a : Array U32 2usize) : 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 2#usize) : Result Unit :=
+def take_array_borrow (a : Array U32 2usize) : Result Unit :=
   Result.ok ()
 
 /- [arrays::take_slice]:
@@ -204,70 +204,67 @@ 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 2#usize) :=
-  Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+def const_array : Result (Array U32 2usize) :=
+  Result.ok (Array.make U32 2usize [ 0u32, 0u32 ])
 
 /- [arrays::const_slice]:
    Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/
 def const_slice : Result Unit :=
   do
-  let _ ←
-    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   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 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_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_slice s
   let (s1, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   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 2#usize) : Result U32 :=
-  Array.index_usize U32 2#usize x 0#usize
+def index_array (x : Array U32 2usize) : Result U32 :=
+  Array.index_usize U32 2usize x 0usize
 
 /- [arrays::index_array_borrow]:
    Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/
-def index_array_borrow (x : Array U32 2#usize) : Result U32 :=
-  Array.index_usize U32 2#usize x 0#usize
+def index_array_borrow (x : Array U32 2usize) : Result U32 :=
+  Array.index_usize U32 2usize x 0usize
 
 /- [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 0#usize
+  Slice.index_usize U32 x 0usize
 
 /- [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 0#usize
+  let i ← Slice.index_usize U32 x 0usize
   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 2#usize [ 0#u32, 0#u32 ])
-  let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
+  let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
   let i2 ← i + i1
-  let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
   let i4 ← i2 + i3
-  let s ←
-    Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let i5 ← index_slice_u32_0 s
   let i6 ← i4 + i5
   let (s1, to_slice_mut_back) ←
-    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
   let i8 ← i6 + i7
   let _ ← to_slice_mut_back s2
@@ -275,35 +272,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 2#usize) : Result Unit :=
+def update_array (x : Array U32 2usize) : Result Unit :=
   do
-  let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
-  let _ ← index_mut_back 1#u32
+  let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
+  let _ ← index_mut_back 1u32
   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 2#usize) : Result (Array U32 2#usize) :=
+  (x : Array U32 2usize) : Result (Array U32 2usize) :=
   do
-  let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
-  index_mut_back 1#u32
+  let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
+  index_mut_back 1u32
 
 /- [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 0#usize
-  index_mut_back 1#u32
+  let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0usize
+  index_mut_back 1u32
 
 /- [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 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 _ ← 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 s1 ← update_mut_slice s
   let _ ← to_slice_mut_back s1
   Result.ok ()
@@ -313,37 +310,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) 4#usize
+    core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize
       (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
       (core.slice.index.SliceIndexRangeUsizeSliceTInst U32))
-      (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ])
-      { start := 1#usize, end_ := 3#usize }
+      (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ])
+      { start := 1usize, end_ := 3usize }
   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 2#usize) : Result U32 :=
-  Array.index_usize U32 2#usize x 0#usize
+def deref_array_borrow (x : Array U32 2usize) : Result U32 :=
+  Array.index_usize U32 2usize x 0usize
 
 /- [arrays::deref_array_mut_borrow]:
    Source: 'tests/src/arrays.rs', lines 222:0-222:54 -/
 def deref_array_mut_borrow
-  (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
+  (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) :=
   do
-  let i ← Array.index_usize U32 2#usize x 0#usize
+  let i ← Array.index_usize U32 2usize x 0usize
   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 2#usize) : Result Unit :=
+def take_array_t (a : Array AB 2usize) : 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 2#usize [ AB.A, AB.B ])
+  take_array_t (Array.make AB 2usize [ AB.A, AB.B ])
 
 /- [arrays::sum]: loop 0:
    Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
@@ -354,14 +351,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 + 1#usize
+    let i3 ← i + 1usize
     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 0#u32 0#usize
+  sum_loop s 0u32 0usize
 
 /- [arrays::sum2]: loop 0:
    Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
@@ -375,7 +372,7 @@ divergent def sum2_loop
     let i3 ← Slice.index_usize U32 s2 i
     let i4 ← i2 + i3
     let sum3 ← sum1 + i4
-    let i5 ← i + 1#usize
+    let i5 ← i + 1usize
     sum2_loop s s2 sum3 i5
   else Result.ok sum1
 
@@ -385,7 +382,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 0#u32 0#usize
+  then sum2_loop s s2 0u32 0usize
   else Result.fail .panic
 
 /- [arrays::f0]:
@@ -393,9 +390,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 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
+    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
   let _ ← to_slice_mut_back s1
   Result.ok ()
 
@@ -404,9 +401,9 @@ def f0 : Result Unit :=
 def f1 : Result Unit :=
   do
   let (_, index_mut_back) ←
-    Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
-      0#usize
-  let _ ← index_mut_back 1#u32
+    Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
+      0usize
+  let _ ← index_mut_back 1u32
   Result.ok ()
 
 /- [arrays::f2]:
@@ -416,8 +413,8 @@ def f2 (i : U32) : Result Unit :=
 
 /- [arrays::f4]:
    Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/
-def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
-  core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
+def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
+  core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
     (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize)
     (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
     { start := y, end_ := z }
@@ -427,34 +424,32 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
 def f3 : Result U32 :=
   do
   let i ←
-    Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
-      0#usize
+    Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize
   let _ ← f2 i
-  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
+  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
   sum2 s s1
 
 /- [arrays::SZ]
    Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/
-def SZ_body : Result Usize := Result.ok 32#usize
+def SZ_body : Result Usize := Result.ok 32usize
 def SZ : Usize := eval_global SZ_body
 
 /- [arrays::f5]:
    Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/
-def f5 (x : Array U32 32#usize) : Result U32 :=
-  Array.index_usize U32 32#usize x 0#usize
+def f5 (x : Array U32 32usize) : Result U32 :=
+  Array.index_usize U32 32usize x 0usize
 
 /- [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 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (_, s1) ← index_mut_slice_u32_0 s
   let (s2, to_slice_mut_back1) ←
-    Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+    Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (_, s3) ← index_mut_slice_u32_0 s2
   let _ ← to_slice_mut_back1 s3
   let _ ← to_slice_mut_back s1
@@ -468,8 +463,8 @@ divergent def zero_slice_loop
   then
     do
     let (_, index_mut_back) ← Slice.index_mut_usize U8 a i
-    let i1 ← i + 1#usize
-    let a1 ← index_mut_back 0#u8
+    let i1 ← i + 1usize
+    let a1 ← index_mut_back 0u8
     zero_slice_loop a1 i1 len
   else Result.ok a
 
@@ -477,14 +472,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 0#usize len
+  zero_slice_loop a 0usize 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 + 1#usize
+       let i1 ← i + 1usize
        iter_mut_slice_loop len i1
   else Result.ok ()
 
@@ -493,7 +488,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 0#usize
+  let _ ← iter_mut_slice_loop len 0usize
   Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
@@ -506,7 +501,7 @@ divergent def sum_mut_slice_loop
     do
     let i2 ← Slice.index_usize U32 a i
     let s1 ← s + i2
-    let i3 ← i + 1#usize
+    let i3 ← i + 1usize
     sum_mut_slice_loop a i3 s1
   else Result.ok s
 
@@ -514,7 +509,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 0#usize 0#u32
+  let i ← sum_mut_slice_loop a 0usize 0u32
   Result.ok (i, a)
 
 end arrays
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 7d8b4714..74344e01 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 + 1#u64
+  let counter1 ← counter + 1u64
   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 := 0#u64 }
+  Result.ok { next_node_id := 0u64 }
 
 /- [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 + 1#u64
+  let i ← self.next_node_id + 1u64
   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 0#u64
+    | betree.UpsertFunState.Sub _ => Result.ok 0u64
   | 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 0#u64
+      else Result.ok 0u64
 
 /- [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 + 1#u64
+    let len1 ← len + 1u64
     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 0#u64
+  betree.List.len_loop T self 0u64
 
 /- [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 > 0#u64
+  if n > 0u64
   then
     match self with
     | betree.List.Cons hd tl =>
       do
-      let n1 ← n - 1#u64
+      let n1 ← n - 1u64
       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 ← 2#u64 * params.split_size
+    let i ← 2u64 * 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 := 0#u64 })
+      root := (betree.Node.Leaf { id := id, size := 0u64 })
     })
 
 /- [betree::betree::{betree::betree::BeTree#6}::apply]:
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 23ec66b4..8884d309 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 >>> 16#usize
-  t <<< 16#usize
+  let t ← a >>> 16usize
+  t <<< 16usize
 
 /- [bitwise::shift_i32]:
    Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
 def shift_i32 (a : I32) : Result I32 :=
   do
-  let t ← a >>> 16#isize
-  t <<< 16#isize
+  let t ← a >>> 16isize
+  t <<< 16isize
 
 /- [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 ecb91c16..a72ac98d 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 0#u32
+def X0_body : Result U32 := Result.ok 0u32
 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 3#u32
+def X2_body : Result U32 := Result.ok 3u32
 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 + 1#u32
+  n + 1u32
 
 /- [constants::X3]
    Source: 'tests/src/constants.rs', lines 18:0-18:17 -/
-def X3_body : Result U32 := incr 32#u32
+def X3_body : Result U32 := incr 32u32
 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 0#u32 1#u32
+def P0_body : Result (U32 × U32) := mk_pair0 0u32 1u32
 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 0#u32 1#u32
+def P1_body : Result (Pair U32 U32) := mk_pair1 0u32 1u32
 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 (0#u32, 1#u32)
+def P2_body : Result (U32 × U32) := Result.ok (0u32, 1u32)
 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 := 0#u32, y := 1#u32 }
+def P3_body : Result (Pair U32 U32) := Result.ok { x := 0u32, y := 1u32 }
 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 2#i32
+def Y_body : Result (Wrap I32) := Wrap.new I32 2i32
 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 3#i32
+def get_z1.Z1_body : Result I32 := Result.ok 3i32
 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 5#i32
+def Q1_body : Result I32 := Result.ok 5i32
 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 3#i32
+def Q3_body : Result I32 := add Q2 3i32
 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 6#u32
+def S1_body : Result U32 := Result.ok 6u32
 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 7#u32 8#u32
+def S4_body : Result (Pair U32 U32) := mk_pair1 7u32 8u32
 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 48ac2062..9d8b085c 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 + 1#u32
+  i + 1u32
 
 /- [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 + 1#u32
+  x + 1u32
 
 /- [demo::use_incr]:
    Source: 'tests/src/demo.rs', lines 27:0-27:17 -/
 def use_incr : Result Unit :=
   do
-  let x ← incr 0#u32
+  let x ← incr 0u32
   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 = 0#u32
+    if i = 0u32
     then Result.ok x
     else do
-         let i1 ← i - 1#u32
+         let i1 ← i - 1u32
          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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (CList.CCons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (CList.CCons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 = 0#i32
-  then Result.ok 0#i32
+  if i = 0i32
+  then Result.ok 0i32
   else do
-       let i1 ← i - 1#i32
+       let i1 ← i - 1i32
        let i2 ← i32_id i1
-       i2 + 1#i32
+       i2 + 1i32
 
 /- [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 + 1#usize
+  let self1 ← self + 1usize
   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 1b1d5cdf..c828720a 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 + 1#u32
+  let i1 ← i + 1u32
   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 612e1848..3c244ee0 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 > 0#usize
+  if n > 0usize
   then
     do
     let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
-    let n1 ← n - 1#usize
+    let n1 ← n - 1usize
     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 := 0#usize,
+      num_entries := 0usize,
       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 32#usize 4#usize 5#usize
+  HashMap.new_with_capacity T 32usize 4usize 5usize
 
 /- [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 + 1#usize
+    let i2 ← i + 1usize
     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 0#usize
-  Result.ok { self with num_entries := 0#usize, slots := hm }
+  let hm ← HashMap.clear_loop T self.slots 0usize
+  Result.ok { self with num_entries := 0usize, 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 + 1#usize
+    let i1 ← self.num_entries + 1usize
     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 + 1#usize
+    let i2 ← i + 1usize
     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 / 2#usize
+  let n1 ← max_usize / 2usize
   let (i, i1) := self.max_load_factor
   let i2 ← n1 / i
   if capacity <= i2
   then
     do
-    let i3 ← capacity * 2#usize
+    let i3 ← capacity * 2usize
     let ntable ← HashMap.new_with_capacity T i3 i i1
-    let p ← HashMap.move_elements T ntable self.slots 0#usize
+    let p ← HashMap.move_elements T ntable self.slots 0usize
     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 - 1#usize
+    let i1 ← self.num_entries - 1usize
     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 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
+  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
   then
     do
-    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
+    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
     then
       do
-      let (x, hm6) ← HashMap.remove U64 hm5 1024#usize
+      let (x, hm6) ← HashMap.remove U64 hm5 1024usize
       match x with
       | none => Result.fail .panic
       | some x1 =>
-        if x1 = 56#u64
+        if x1 = 56u64
         then
           do
-          let i2 ← HashMap.get U64 hm6 0#usize
-          if i2 = 42#u64
+          let i2 ← HashMap.get U64 hm6 0usize
+          if i2 = 42u64
           then
             do
-            let i3 ← HashMap.get U64 hm6 128#usize
-            if i3 = 18#u64
+            let i3 ← HashMap.get U64 hm6 128usize
+            if i3 = 18u64
             then
               do
-              let i4 ← HashMap.get U64 hm6 1056#usize
-              if i4 = 256#u64
+              let i4 ← HashMap.get U64 hm6 1056usize
+              if i4 = 256u64
               then Result.ok ()
               else Result.fail .panic
             else Result.fail .panic
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 199605d5..567d2b44 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 + 1#u32
+       let i1 ← i + 1u32
        sum_loop max i1 s1
-  else s * 2#u32
+  else s * 2u32
 
 /- [loops::sum]:
    Source: 'tests/src/loops.rs', lines 8:0-8:27 -/
 def sum (max : U32) : Result U32 :=
-  sum_loop max 0#u32 0#u32
+  sum_loop max 0u32 0u32
 
 /- [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 + 1#u32
+    let mi ← i + 1u32
     sum_with_mut_borrows_loop max mi ms
-  else s * 2#u32
+  else s * 2u32
 
 /- [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 0#u32 0#u32
+  sum_with_mut_borrows_loop max 0u32 0u32
 
 /- [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 + 1#u32
+    let i1 ← i + 1u32
     let s1 ← s + i1
     sum_with_shared_borrows_loop max i1 s1
-  else s * 2#u32
+  else s * 2u32
 
 /- [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 0#u32 0#u32
+  sum_with_shared_borrows_loop max 0u32 0u32
 
 /- [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 + 1#usize
+    let i2 ← i + 1usize
     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 0#usize 0#u32
+  sum_array_loop N a 0usize 0u32
 
 /- [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 + 1#usize
-    let v1 ← index_mut_back 0#u32
+    let i2 ← i + 1usize
+    let v1 ← index_mut_back 0u32
     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 0#usize
+  clear_loop v 0usize
 
 /- [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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 = 0#u32
+    if i = 0u32
     then Result.ok x
     else do
-         let i1 ← i - 1#u32
+         let i1 ← i - 1u32
          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 0#usize
+      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
   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 0#usize
+      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
   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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 = 0#u32
+    if i = 0u32
     then Result.ok x
     else do
-         let i1 ← i - 1#u32
+         let i1 ← i - 1u32
          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 = 0#u32
+      if i = 0u32
       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 - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then Result.ok (x0, x1)
       else do
-           let i1 ← i - 1#u32
+           let i1 ← i - 1u32
            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 = 0#u32
+      if i = 0u32
       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 - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then Result.ok (x0, x1)
       else
         do
-        let i1 ← i - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl0)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl0)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl1)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1#u32
+        let i1 ← i - 1u32
         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 = 0#u32
+      if i = 0u32
       then
         let back := fun ret => Result.ok (List.Cons ret tl1)
         Result.ok ((x0, x1), back)
       else
         do
-        let i1 ← i - 1#u32
+        let i1 ← i - 1u32
         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 > 0#u32
+  if i > 0u32
   then do
-       let i1 ← i - 1#u32
+       let i1 ← i - 1u32
        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 > 0#u32
+  if i > 0u32
   then do
-       let i1 ← i - 1#u32
+       let i1 ← i - 1u32
        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 + 1#u32
+  let a1 ← a + 1u32
   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 > 0#u32
+  if i > 0u32
   then do
-       let i1 ← i - 1#u32
+       let i1 ← i - 1u32
        ignore_input_shared_borrow_loop i1
   else Result.ok ()
 
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 3e3a558b..34f899b1 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
-  | 0#u32 => Result.ok 0#u32
-  | 1#u32 => Result.ok 1#u32
-  | _ => Result.ok 2#u32
+  | 0u32 => Result.ok 0u32
+  | 1u32 => Result.ok 1u32
+  | _ => Result.ok 2u32
 
 end matches
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index f0438050..01f6736c 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 _ ← 23#u32 + 44#u32
+  let _ ← 23u32 + 44u32
   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 4#u32 3#u32
-  let y ← get_max 10#u32 11#u32
+  let x ← get_max 4u32 3u32
+  let y ← get_max 10u32 11u32
   let z ← x + y
-  if z = 15#u32
+  if z = 15u32
   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 ← -. 3#i32
-  if y = (-3)#i32
+  let y ← -. 3i32
+  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 1#i32 = 1#i32
+  if 1i32 = 1i32
   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 2#i32 = 2#i32
+  if 2i32 = 2i32
   then
-    if 0#i32 = 0#i32
+    if 0i32 = 0i32
     then
-      if 2#i32 = 2#i32
-      then if 2#i32 = 2#i32
+      if 2i32 = 2i32
+      then if 2i32 = 2i32
            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 0#i32
-  let b ← deref_mut_back 1#i32
+  let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0i32
+  let b ← deref_mut_back 1i32
   let x ← alloc.boxed.Box.deref I32 b
-  if x = 1#i32
+  if x = 1i32
   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 0#i32
-  if 0#i32 = y
+  let y ← copy_int 0i32
+  if 0i32 = 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 0#i32 List.Nil)
+  let b ← is_cons I32 (List.Cons 0i32 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 0#i32 List.Nil)
+  let p ← split_list I32 (List.Cons 0i32 List.Nil)
   let (hd, _) := p
-  if hd = 0#i32
+  if hd = 0i32
   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 0#i32 0#i32
-  let z1 ← z + 1#i32
-  if z1 = 1#i32
+  let (z, choose_back) ← choose I32 true 0i32 0i32
+  let z1 ← z + 1i32
+  if z1 = 1i32
   then
     do
     let (x, y) ← choose_back z1
-    if x = 1#i32
-    then if y = 0#i32
+    if x = 1i32
+    then if y = 0i32
          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
-                      1#u32 + i
-  | List.Nil => Result.ok 0#u32
+                      1u32 + i
+  | List.Nil => Result.ok 0u32
 
 /- [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 = 0#u32
+    if i = 0u32
     then Result.ok x
     else do
-         let i1 ← i - 1#u32
+         let i1 ← i - 1u32
          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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 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
+  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
   then
     do
-    let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
-    if i1 = 0#i32
+    let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32
+    if i1 = 0i32
     then
       do
-      let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
-      if i2 = 1#i32
+      let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32
+      if i2 = 1i32
       then
         do
-        let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
-        if i3 = 2#i32
+        let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32
+        if i3 = 2i32
         then
           do
           let (_, list_nth_mut_back) ←
-            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
+            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
           then
             do
-            let i5 ← list_nth_shared I32 ls 1#u32
-            if i5 = 3#i32
+            let i5 ← list_nth_shared I32 ls 1u32
+            if i5 = 3i32
             then
               do
-              let i6 ← list_nth_shared I32 ls 2#u32
-              if i6 = 2#i32
+              let i6 ← list_nth_shared I32 ls 2u32
+              if i6 = 2i32
               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 := (1#u32, 2#u32) }
+  Result.ok { p := (1u32, 2u32) }
 
 /- [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 := (1#i16, 2#i16) }
+  Result.ok { p := (1i16, 2i16) }
 
 /- [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 := (1#u64, 2#i64) }
+  Result.ok { p := (1u64, 2i64) }
 
 /- [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 := 1#u32, y := 2#u32 } }
+  Result.ok { p := { x := 1u32, y := 2u32 } }
 
 /- [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 = 1#u32
+  if i = 1u32
   then
     do
     let swt1 ← new_tuple2
     let (i1, _) := swt1.p
-    if i1 = 1#i16
+    if i1 = 1i16
     then
       do
       let swt2 ← new_tuple3
       let (i2, _) := swt2.p
-      if i2 = 1#u64
+      if i2 = 1u64
       then
         do
         let swp ← new_pair1
-        if swp.p.x = 1#u32
+        if swp.p.x = 1u32
         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 1#u32
-  if y = 0#u32
-  then Result.ok 2#u32
+  let (y, _) := core.mem.replace U32 px 1u32
+  if y = 0u32
+  then Result.ok 2u32
   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 0#u32
-  else Result.ok 1#u32
+  then Result.ok 0u32
+  else Result.ok 1u32
 
 /- [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 0#u32
+  Result.ok 0u32
 
 /- [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 1#u32
-  | List.Nil => Result.ok 0#u32
+  | List.Cons _ _ => Result.ok 1u32
+  | List.Nil => Result.ok 0u32
 
 /- [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 0#u32
+  Result.ok 0u32
 
 /- [no_nested_borrows::incr]:
    Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/
 def incr (x : U32) : Result U32 :=
-  x + 1#u32
+  x + 1u32
 
 /- [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 + 1#u32
+  let x1 ← x + 1u32
   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 (1#u32, i)
+  Result.ok (1u32, 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 (1#u32, i)
+  Result.ok (1u32, 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 03b96903..400406f1 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 + 1#i32
+  x + 1i32
 
 /- [paper::test_incr]:
    Source: 'tests/src/paper.rs', lines 11:0-11:18 -/
 def test_incr : Result Unit :=
   do
-  let x ← ref_incr 0#i32
-  if x = 1#i32
+  let x ← ref_incr 0i32
+  if x = 1i32
   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 0#i32 0#i32
-  let z1 ← z + 1#i32
-  if z1 = 1#i32
+  let (z, choose_back) ← choose I32 true 0i32 0i32
+  let z1 ← z + 1i32
+  if z1 = 1i32
   then
     do
     let (x, y) ← choose_back z1
-    if x = 1#i32
-    then if y = 0#i32
+    if x = 1i32
+    then if y = 0i32
          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 = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       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 0#i32
+  | List.Nil => Result.ok 0i32
 
 /- [paper::test_nth]:
    Source: 'tests/src/paper.rs', lines 71:0-71:17 -/
 def test_nth : Result Unit :=
   do
-  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 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 l2 ← list_nth_mut_back x1
   let i ← sum l2
-  if i = 7#i32
+  if i = 7i32
   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 + 1#u32
+  let pz1 ← pz + 1u32
   let (px1, _) ← choose_back pz1
   Result.ok px1
 
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 0dd692fe..1cd8644b 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 > 0#u64)
+  Result.ok (self > 0u64)
 
 /- 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 > 1#u64)
+  Result.ok (self > 1u64)
 
 /- 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 > 0#u64
-  then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
+  if x1 > 0u64
+  then TestType.test.TestTraittraitsTestTypetestTestType1.test 0u64
   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 32#usize
+  Result.ok 32usize
 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 12#usize
+def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12usize
 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 32#usize) : Result U64 :=
+def WithConstTyBool32.f (i : U64) (a : Array U8 32usize) : 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 32#usize := {
+def WithConstTyBool32 : WithConstTy Bool 32usize := {
   LEN1 := WithConstTyBool32.LEN1
-  LEN2 := WithConstTy.LEN2_default Bool 32#usize
+  LEN2 := WithConstTy.LEN2_default Bool 32usize
   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 32#usize) (_x : U32) :
+  (T : Type) (WithConstTyT32Inst : WithConstTy T 32usize) (_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 0#usize
+  Result.ok 0usize
 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 0#i32)
+  Result.ok (core.result.Result.Err 0i32)
 def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
   eval_global (Foo.FOO_body T U TraitInst)
 
-- 
cgit v1.2.3


From fe59d3afe131e9f83cbdf73b1c8089ad090d92fb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 16:18:05 +0200
Subject: Update CoreConvertNum.lean

---
 backends/lean/Base/Primitives/CoreConvertNum.lean | 44 +++++++++++------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index eb456a96..bc3db8b2 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -18,40 +18,40 @@ namespace num -- core.convert.num
 
 -- Conversions
 def FromUsizeBool.from (b : Bool) : Usize :=
-  if b then 1#usize else 0#usize
+  if b then 1usize else 0usize
 
 def FromU8Bool.from (b : Bool) : U8 :=
-  if b then 1#u8 else 0#u8
+  if b then 1u8 else 0u8
 
 def FromU16Bool.from (b : Bool) : U16 :=
-  if b then 1#u16 else 0#u16
+  if b then 1u16 else 0u16
 
 def FromU32Bool.from (b : Bool) : U32 :=
-  if b then 1#u32 else 0#u32
+  if b then 1u32 else 0u32
 
 def FromU64Bool.from (b : Bool) : U64 :=
-  if b then 1#u64 else 0#u64
+  if b then 1u64 else 0u64
 
 def FromU128Bool.from (b : Bool) : U128 :=
-  if b then 1#u128 else 0#u128
+  if b then 1u128 else 0u128
 
 def FromIsizeBool.from (b : Bool) : Isize :=
-  if b then 1#isize else 0#isize
+  if b then 1isize else 0isize
 
 def FromI8Bool.from (b : Bool) : I8 :=
-  if b then 1#i8 else 0#i8
+  if b then 1i8 else 0i8
 
 def FromI16Bool.from (b : Bool) : I16 :=
-  if b then 1#i16 else 0#i16
+  if b then 1i16 else 0i16
 
 def FromI32Bool.from (b : Bool) : I32 :=
-  if b then 1#i32 else 0#i32
+  if b then 1i32 else 0i32
 
 def FromI64Bool.from (b : Bool) : I64 :=
-  if b then 1#i64 else 0#i64
+  if b then 1i64 else 0i64
 
 def FromI128Bool.from (b : Bool) : I128 :=
-  if b then 1#i128 else 0#i128
+  if b then 1i128 else 0i128
 
 def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
 
@@ -259,18 +259,18 @@ def FromI128I128 : core.convert.From I128 I128 := {
 }
 
 -- to_le_bytes
-def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
-def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
-def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
-def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
-def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128usize := sorry
 
 -- to_be_bytes
-def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
-def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
-def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
-def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
-def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128usize := sorry
 
 end core.convert
 
-- 
cgit v1.2.3


From f05a0faf14fdd558039da52624d57028eb64f9fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 16:54:24 +0200
Subject: Fix some mistakes

---
 compiler/ExtractBase.ml         |  2 ++
 tests/lean/Arrays.lean          |  4 ++--
 tests/lean/Demo/Properties.lean |  4 ++--
 tests/lean/Tutorial.lean        | 22 +++++++++++-----------
 4 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4aac270f..8fe36d5b 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1016,6 +1016,8 @@ let keywords () =
           "where";
           "with";
         ]
+        @ (* This comes from the scalar notations: `1u32`, etc. *)
+        List.map StringUtils.lowercase_first_letter all_int_names
     | HOL4 ->
         [
           "Axiom";
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 70b4a26b..5f50e580 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -266,9 +266,9 @@ def index_all : Result U32 :=
   let (s1, to_slice_mut_back) ←
     Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
-  let i8 ← i6 + i7
+  let i9 ← i6 + i7
   let _ ← to_slice_mut_back s2
-  Result.ok i8
+  Result.ok i9
 
 /- [arrays::update_array]:
    Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index abdc2985..67023727 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp_all; scalar_tac
   | CCons hd tl =>
     simp_all
-    if hi: i = 0#u32 then
+    if hi: i = 0u32 then
       simp_all
     else
       simp_all
@@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0#i32 then
+  if hx : x = 0i32 then
     simp_all
   else
     simp_all
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 94b70991..7d347277 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -17,7 +17,7 @@ namespace Tutorial
 
 def mul2_add1 (x : U32) : Result U32 := do
   let x1 ← x + x
-  let x2 ← x1 + 1#u32
+  let x2 ← x1 + 1u32
   ok x2
 
 /- There are several things to note.
@@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do
    Because Rust programs manipulate machine integers which occupy a fixed
    size in memory, we model integers by using types like [U32], which is
    the type of integers which take their values between 0 and 2^32 - 1 (inclusive).
-   [1#u32] is simply the constant 1 (seen as a [U32]).
+   [1u32] is simply the constant 1 (seen as a [U32]).
 
    You can see a definition or its type by using the [#print] and [#check] commands.
    It is also possible to jump to definitions (right-click + "Go to Definition"
@@ -229,10 +229,10 @@ open CList
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CCons x tl =>
-    if i = 0#u32
+    if i = 0u32
     then ok x
     else do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       list_nth T tl i1
   | CNil => fail Error.panic
 
@@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp only []
     -- Perform a case disjunction on [i].
     -- The notation [hi : ...] allows us to introduce an assumption in the
-    -- context, to remember the fact that in the branches we have [i = 0#u32]
-    -- and [¬ i = 0#u32].
-    if hi: i = 0#u32 then
+    -- context, to remember the fact that in the branches we have [i = 0u32]
+    -- and [¬ i = 0u32].
+    if hi: i = 0u32 then
       -- We can finish the proof simply by using the simplifier.
       -- We decompose the proof into several calls on purpose, so that it is
       -- easier to understand what is going on.
@@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
    annotates it with the [divergent] keyword.
  -/
 divergent def i32_id (x : I32) : Result I32 :=
-  if x = 0#i32 then ok 0#i32
+  if x = 0i32 then ok 0i32
   else do
-    let x1 ← x - 1#i32
+    let x1 ← x - 1i32
     let x2 ← i32_id x1
-    x2 + 1#i32
+    x2 + 1i32
 
 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0#i32 then
+  if hx : x = 0i32 then
     simp_all
   else
     simp [hx]
-- 
cgit v1.2.3


From 8ca43c32b30c03cc3fde51736ea5884dfd1c2c50 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:14 +0200
Subject: Revert "Fix some mistakes"

This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd.
---
 compiler/ExtractBase.ml         |  2 --
 tests/lean/Arrays.lean          |  4 ++--
 tests/lean/Demo/Properties.lean |  4 ++--
 tests/lean/Tutorial.lean        | 22 +++++++++++-----------
 4 files changed, 15 insertions(+), 17 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8fe36d5b..4aac270f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1016,8 +1016,6 @@ let keywords () =
           "where";
           "with";
         ]
-        @ (* This comes from the scalar notations: `1u32`, etc. *)
-        List.map StringUtils.lowercase_first_letter all_int_names
     | HOL4 ->
         [
           "Axiom";
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 5f50e580..70b4a26b 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -266,9 +266,9 @@ def index_all : Result U32 :=
   let (s1, to_slice_mut_back) ←
     Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
-  let i9 ← i6 + i7
+  let i8 ← i6 + i7
   let _ ← to_slice_mut_back s2
-  Result.ok i9
+  Result.ok i8
 
 /- [arrays::update_array]:
    Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index 67023727..abdc2985 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp_all; scalar_tac
   | CCons hd tl =>
     simp_all
-    if hi: i = 0u32 then
+    if hi: i = 0#u32 then
       simp_all
     else
       simp_all
@@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0i32 then
+  if hx : x = 0#i32 then
     simp_all
   else
     simp_all
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 7d347277..94b70991 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -17,7 +17,7 @@ namespace Tutorial
 
 def mul2_add1 (x : U32) : Result U32 := do
   let x1 ← x + x
-  let x2 ← x1 + 1u32
+  let x2 ← x1 + 1#u32
   ok x2
 
 /- There are several things to note.
@@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do
    Because Rust programs manipulate machine integers which occupy a fixed
    size in memory, we model integers by using types like [U32], which is
    the type of integers which take their values between 0 and 2^32 - 1 (inclusive).
-   [1u32] is simply the constant 1 (seen as a [U32]).
+   [1#u32] is simply the constant 1 (seen as a [U32]).
 
    You can see a definition or its type by using the [#print] and [#check] commands.
    It is also possible to jump to definitions (right-click + "Go to Definition"
@@ -229,10 +229,10 @@ open CList
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CCons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then ok x
     else do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       list_nth T tl i1
   | CNil => fail Error.panic
 
@@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp only []
     -- Perform a case disjunction on [i].
     -- The notation [hi : ...] allows us to introduce an assumption in the
-    -- context, to remember the fact that in the branches we have [i = 0u32]
-    -- and [¬ i = 0u32].
-    if hi: i = 0u32 then
+    -- context, to remember the fact that in the branches we have [i = 0#u32]
+    -- and [¬ i = 0#u32].
+    if hi: i = 0#u32 then
       -- We can finish the proof simply by using the simplifier.
       -- We decompose the proof into several calls on purpose, so that it is
       -- easier to understand what is going on.
@@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
    annotates it with the [divergent] keyword.
  -/
 divergent def i32_id (x : I32) : Result I32 :=
-  if x = 0i32 then ok 0i32
+  if x = 0#i32 then ok 0#i32
   else do
-    let x1 ← x - 1i32
+    let x1 ← x - 1#i32
     let x2 ← i32_id x1
-    x2 + 1i32
+    x2 + 1#i32
 
 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0i32 then
+  if hx : x = 0#i32 then
     simp_all
   else
     simp [hx]
-- 
cgit v1.2.3


From dd2b973a86680308807d7f26aff81d3310550f84 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:23 +0200
Subject: Revert "Update CoreConvertNum.lean"

This reverts commit fe59d3afe131e9f83cbdf73b1c8089ad090d92fb.
---
 backends/lean/Base/Primitives/CoreConvertNum.lean | 44 +++++++++++------------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/backends/lean/Base/Primitives/CoreConvertNum.lean b/backends/lean/Base/Primitives/CoreConvertNum.lean
index bc3db8b2..eb456a96 100644
--- a/backends/lean/Base/Primitives/CoreConvertNum.lean
+++ b/backends/lean/Base/Primitives/CoreConvertNum.lean
@@ -18,40 +18,40 @@ namespace num -- core.convert.num
 
 -- Conversions
 def FromUsizeBool.from (b : Bool) : Usize :=
-  if b then 1usize else 0usize
+  if b then 1#usize else 0#usize
 
 def FromU8Bool.from (b : Bool) : U8 :=
-  if b then 1u8 else 0u8
+  if b then 1#u8 else 0#u8
 
 def FromU16Bool.from (b : Bool) : U16 :=
-  if b then 1u16 else 0u16
+  if b then 1#u16 else 0#u16
 
 def FromU32Bool.from (b : Bool) : U32 :=
-  if b then 1u32 else 0u32
+  if b then 1#u32 else 0#u32
 
 def FromU64Bool.from (b : Bool) : U64 :=
-  if b then 1u64 else 0u64
+  if b then 1#u64 else 0#u64
 
 def FromU128Bool.from (b : Bool) : U128 :=
-  if b then 1u128 else 0u128
+  if b then 1#u128 else 0#u128
 
 def FromIsizeBool.from (b : Bool) : Isize :=
-  if b then 1isize else 0isize
+  if b then 1#isize else 0#isize
 
 def FromI8Bool.from (b : Bool) : I8 :=
-  if b then 1i8 else 0i8
+  if b then 1#i8 else 0#i8
 
 def FromI16Bool.from (b : Bool) : I16 :=
-  if b then 1i16 else 0i16
+  if b then 1#i16 else 0#i16
 
 def FromI32Bool.from (b : Bool) : I32 :=
-  if b then 1i32 else 0i32
+  if b then 1#i32 else 0#i32
 
 def FromI64Bool.from (b : Bool) : I64 :=
-  if b then 1i64 else 0i64
+  if b then 1#i64 else 0#i64
 
 def FromI128Bool.from (b : Bool) : I128 :=
-  if b then 1i128 else 0i128
+  if b then 1#i128 else 0#i128
 
 def FromUsizeU8.from (x : U8) : Usize := ⟨ x.val, by scalar_tac, by scalar_tac ⟩
 
@@ -259,18 +259,18 @@ def FromI128I128 : core.convert.From I128 I128 := {
 }
 
 -- to_le_bytes
-def core.num.U8.to_le_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_le_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_le_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_le_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_le_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_le_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_le_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_le_bytes (x : U128) : Array U8 128#usize := sorry
 
 -- to_be_bytes
-def core.num.U8.to_be_bytes (x : U8) : Array U8 1usize := sorry
-def core.num.U16.to_be_bytes (x : U16) : Array U8 2usize := sorry
-def core.num.U32.to_be_bytes (x : U32) : Array U8 4usize := sorry
-def core.num.U64.to_be_bytes (x : U64) : Array U8 8usize := sorry
-def core.num.U128.to_be_bytes (x : U128) : Array U8 128usize := sorry
+def core.num.U8.to_be_bytes (x : U8) : Array U8 1#usize := sorry
+def core.num.U16.to_be_bytes (x : U16) : Array U8 2#usize := sorry
+def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
+def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
+def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
 
 end core.convert
 
-- 
cgit v1.2.3


From d85d160ae9736f50d9c043b411c5a831f1fbb964 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:35 +0200
Subject: Revert "Regenerate the tests"

This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e.
---
 tests/lean/Arrays.lean          | 225 ++++++++++++++++++++--------------------
 tests/lean/Betree/Funs.lean     |  22 ++--
 tests/lean/Bitwise.lean         |   8 +-
 tests/lean/Constants.lean       |  28 ++---
 tests/lean/Demo/Demo.lean       |  28 ++---
 tests/lean/External/Funs.lean   |   2 +-
 tests/lean/Hashmap/Funs.lean    |  62 +++++------
 tests/lean/Loops.lean           |  94 ++++++++---------
 tests/lean/Matches.lean         |   6 +-
 tests/lean/NoNestedBorrows.lean | 138 ++++++++++++------------
 tests/lean/Paper.lean           |  34 +++---
 tests/lean/Traits.lean          |  24 ++---
 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)
 
-- 
cgit v1.2.3


From d36736fa4e7eb9f42f35303b8080d17ddbee92d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:52 +0200
Subject: Revert "Update the scalar notation for the Lean backend"

This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
---
 backends/lean/Base/Primitives/Scalar.lean | 50 +++++++++++++++----------------
 compiler/ExtractTypes.ml                  |  2 +-
 2 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 5f14a14f..157ade2c 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -313,13 +313,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
 /- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `u32` (which
+   This is particularly useful once we introduce notations like `#u32` (which
    desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
    Example:
    ```
    match x with
-   | 0u32 => ...
-   | 1u32 => ...
+   | 0#u32 => ...
+   | 1#u32 => ...
    | ...
    ```
  -/
@@ -328,7 +328,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   { val := x, hmin := h.left, hmax := h.right }
 
 -- The definitions below are used later to introduce nice syntax for constants,
--- like `1u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
+-- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
 
 class InBounds (ty : ScalarTy) (x : Int) :=
   hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
@@ -1281,38 +1281,38 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 @[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
 @[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
 
-postfix:max "isize" => Isize.ofInt
-postfix:max "i8"    => I8.ofInt
-postfix:max "i16"   => I16.ofInt
-postfix:max "i32"   => I32.ofInt
-postfix:max "i64"   => I64.ofInt
-postfix:max "i128"  => I128.ofInt
-postfix:max "usize" => Usize.ofInt
-postfix:max "u8"    => U8.ofInt
-postfix:max "u16"   => U16.ofInt
-postfix:max "u32"   => U32.ofInt
-postfix:max "u64"   => U64.ofInt
-postfix:max "u128"  => U128.ofInt
+postfix:max "#isize" => Isize.ofInt
+postfix:max "#i8"    => I8.ofInt
+postfix:max "#i16"   => I16.ofInt
+postfix:max "#i32"   => I32.ofInt
+postfix:max "#i64"   => I64.ofInt
+postfix:max "#i128"  => I128.ofInt
+postfix:max "#usize" => Usize.ofInt
+postfix:max "#u8"    => U8.ofInt
+postfix:max "#u16"   => U16.ofInt
+postfix:max "#u32"   => U32.ofInt
+postfix:max "#u64"   => U64.ofInt
+postfix:max "#u128"  => U128.ofInt
 
 /- Testing the notations -/
-example := 0u32
-example := 1u32
-example := 1i32
-example := 0isize
-example := (-1)isize
+example := 0#u32
+example := 1#u32
+example := 1#i32
+example := 0#isize
+example := (-1)#isize
 example (x : U32) : Bool :=
   match x with
-  | 0u32 => true
+  | 0#u32 => true
   | _ => false
 
 example (x : U32) : Bool :=
   match x with
-  | 1u32 => true
+  | 1#u32 => true
   | _ => false
 
 example (x : I32) : Bool :=
   match x with
-  | (-1)i32 => true
+  | (-1)#i32 => true
   | _ => false
 
 -- Notation for pattern matching
@@ -1334,7 +1334,7 @@ example {ty} (x : Scalar ty) : Bool :=
   | _ => false
 
 -- Testing the notations
-example : Result Usize := 0usize + 1usize
+example : Result Usize := 0#usize + 1#usize
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 5446f912..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
               let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt iname
+              F.pp_print_string fmt ("#" ^ iname)
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
-- 
cgit v1.2.3