Regenerate the translated files for Lean

4 files changed, 108 insertions, 117 deletions

diff --git a/tests/lean/hashmap/Hashmap/Clauses/Clauses.lean b/tests/lean/hashmap/Hashmap/Clauses/Clauses.lean
index fad5c11a..197b0a6a 100644
--- a/tests/lean/hashmap/Hashmap/Clauses/Clauses.lean
+++ b/tests/lean/hashmap/Hashmap/Clauses/Clauses.lean
@@ -1,11 +1,11 @@
--- [hashmap]: the decreases clauses
+-- [hashmap]: templates for the decreases clauses
 import Base.Primitives
 import Hashmap.Types
 
 /- [hashmap::HashMap::{0}::allocate_slots]: termination measure -/
 @[simp]
 def hash_map_allocate_slots_loop_terminates (T : Type) (slots : Vec (list_t T))
-  (n : USize) :=
+  (n : Usize) :=
   (slots, n)
 
 /- [hashmap::HashMap::{0}::allocate_slots]: decreases_by tactic -/
@@ -16,7 +16,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::clear]: termination measure -/
 @[simp]
 def hash_map_clear_loop_terminates (T : Type) (slots : Vec (list_t T))
-  (i : USize) :=
+  (i : Usize) :=
   (slots, i)
 
 /- [hashmap::HashMap::{0}::clear]: decreases_by tactic -/
@@ -26,7 +26,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::insert_in_list]: termination measure -/
 @[simp]
-def hash_map_insert_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_insert_in_list_loop_terminates (T : Type) (key : Usize)
   (value : T) (ls : list_t T) :=
   (key, value, ls)
 
@@ -51,7 +51,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::move_elements]: termination measure -/
 @[simp]
 def hash_map_move_elements_loop_terminates (T : Type) (ntable : hash_map_t T)
-  (slots : Vec (list_t T)) (i : USize) :=
+  (slots : Vec (list_t T)) (i : Usize) :=
   (ntable, slots, i)
 
 /- [hashmap::HashMap::{0}::move_elements]: decreases_by tactic -/
@@ -62,7 +62,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/
 @[simp]
-def hash_map_contains_key_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_contains_key_in_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
@@ -74,7 +74,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::get_in_list]: termination measure -/
 @[simp]
-def hash_map_get_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_get_in_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
@@ -86,7 +86,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/
 @[simp]
 def hash_map_get_mut_in_list_loop_terminates (T : Type) (ls : list_t T)
-  (key : USize) :=
+  (key : Usize) :=
   (ls, key)
 
 /- [hashmap::HashMap::{0}::get_mut_in_list]: decreases_by tactic -/
@@ -96,7 +96,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::remove_from_list]: termination measure -/
 @[simp]
-def hash_map_remove_from_list_loop_terminates (T : Type) (key : USize)
+def hash_map_remove_from_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
diff --git a/tests/lean/hashmap/Hashmap/Clauses/Template.lean b/tests/lean/hashmap/Hashmap/Clauses/Template.lean
index 7ba079f2..560592c8 100644
--- a/tests/lean/hashmap/Hashmap/Clauses/Template.lean
+++ b/tests/lean/hashmap/Hashmap/Clauses/Template.lean
@@ -6,7 +6,7 @@ import Hashmap.Types
 /- [hashmap::HashMap::{0}::allocate_slots]: termination measure -/
 @[simp]
 def hash_map_allocate_slots_loop_terminates (T : Type) (slots : Vec (list_t T))
-  (n : USize) :=
+  (n : Usize) :=
   (slots, n)
 
 /- [hashmap::HashMap::{0}::allocate_slots]: decreases_by tactic -/
@@ -17,7 +17,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::clear]: termination measure -/
 @[simp]
 def hash_map_clear_loop_terminates (T : Type) (slots : Vec (list_t T))
-  (i : USize) :=
+  (i : Usize) :=
   (slots, i)
 
 /- [hashmap::HashMap::{0}::clear]: decreases_by tactic -/
@@ -27,7 +27,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::insert_in_list]: termination measure -/
 @[simp]
-def hash_map_insert_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_insert_in_list_loop_terminates (T : Type) (key : Usize)
   (value : T) (ls : list_t T) :=
   (key, value, ls)
 
@@ -52,7 +52,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::move_elements]: termination measure -/
 @[simp]
 def hash_map_move_elements_loop_terminates (T : Type) (ntable : hash_map_t T)
-  (slots : Vec (list_t T)) (i : USize) :=
+  (slots : Vec (list_t T)) (i : Usize) :=
   (ntable, slots, i)
 
 /- [hashmap::HashMap::{0}::move_elements]: decreases_by tactic -/
@@ -63,7 +63,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::contains_key_in_list]: termination measure -/
 @[simp]
-def hash_map_contains_key_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_contains_key_in_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
@@ -75,7 +75,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::get_in_list]: termination measure -/
 @[simp]
-def hash_map_get_in_list_loop_terminates (T : Type) (key : USize)
+def hash_map_get_in_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
@@ -87,7 +87,7 @@ macro_rules
 /- [hashmap::HashMap::{0}::get_mut_in_list]: termination measure -/
 @[simp]
 def hash_map_get_mut_in_list_loop_terminates (T : Type) (ls : list_t T)
-  (key : USize) :=
+  (key : Usize) :=
   (ls, key)
 
 /- [hashmap::HashMap::{0}::get_mut_in_list]: decreases_by tactic -/
@@ -97,7 +97,7 @@ macro_rules
 
 /- [hashmap::HashMap::{0}::remove_from_list]: termination measure -/
 @[simp]
-def hash_map_remove_from_list_loop_terminates (T : Type) (key : USize)
+def hash_map_remove_from_list_loop_terminates (T : Type) (key : Usize)
   (ls : list_t T) :=
   (key, ls)
 
diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 535ac9b2..77b1a157 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -5,19 +5,19 @@ import Hashmap.Types
 import Hashmap.Clauses.Clauses
 
 /- [hashmap::hash_key] -/
-def hash_key_fwd (k : USize) : Result USize :=
+def hash_key_fwd (k : Usize) : Result Usize :=
   Result.ret k
 
 /- [hashmap::HashMap::{0}::allocate_slots] -/
 def hash_map_allocate_slots_loop_fwd
-  (T : Type) (slots : Vec (list_t T)) (n : USize) :
+  (T : Type) (slots : Vec (list_t T)) (n : Usize) :
   (Result (Vec (list_t T)))
   :=
-  if h: n > (USize.ofNatCore 0 (by intlit))
+  if h: n > (Usize.ofInt 0 (by intlit))
   then
     do
       let slots0 ← vec_push_back (list_t T) slots list_t.Nil
-      let n0 ← USize.checked_sub n (USize.ofNatCore 1 (by intlit))
+      let n0 ← n - (Usize.ofInt 1 (by intlit))
       hash_map_allocate_slots_loop_fwd T slots0 n0
   else Result.ret slots
 termination_by hash_map_allocate_slots_loop_fwd slots n =>
@@ -26,23 +26,23 @@ decreasing_by hash_map_allocate_slots_loop_decreases slots n
 
 /- [hashmap::HashMap::{0}::allocate_slots] -/
 def hash_map_allocate_slots_fwd
-  (T : Type) (slots : Vec (list_t T)) (n : USize) : Result (Vec (list_t T)) :=
+  (T : Type) (slots : Vec (list_t T)) (n : Usize) : Result (Vec (list_t T)) :=
   hash_map_allocate_slots_loop_fwd T slots n
 
 /- [hashmap::HashMap::{0}::new_with_capacity] -/
 def hash_map_new_with_capacity_fwd
-  (T : Type) (capacity : USize) (max_load_dividend : USize)
-  (max_load_divisor : USize) :
+  (T : Type) (capacity : Usize) (max_load_dividend : Usize)
+  (max_load_divisor : Usize) :
   Result (hash_map_t T)
   :=
   do
     let v := vec_new (list_t T)
     let slots ← hash_map_allocate_slots_fwd T v capacity
-    let i ← USize.checked_mul capacity max_load_dividend
-    let i0 ← USize.checked_div i max_load_divisor
+    let i ← capacity * max_load_dividend
+    let i0 ← i / max_load_divisor
     Result.ret
       {
-        hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
+        hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
         hash_map_max_load_factor := (max_load_dividend, max_load_divisor),
         hash_map_max_load := i0,
         hash_map_slots := slots
@@ -50,19 +50,19 @@ def hash_map_new_with_capacity_fwd
 
 /- [hashmap::HashMap::{0}::new] -/
 def hash_map_new_fwd (T : Type) : Result (hash_map_t T) :=
-  hash_map_new_with_capacity_fwd T (USize.ofNatCore 32 (by intlit))
-    (USize.ofNatCore 4 (by intlit)) (USize.ofNatCore 5 (by intlit))
+  hash_map_new_with_capacity_fwd T (Usize.ofInt 32 (by intlit))
+    (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit))
 
 /- [hashmap::HashMap::{0}::clear] -/
 def hash_map_clear_loop_fwd_back
-  (T : Type) (slots : Vec (list_t T)) (i : USize) :
+  (T : Type) (slots : Vec (list_t T)) (i : Usize) :
   (Result (Vec (list_t T)))
   :=
   let i0 := vec_len (list_t T) slots
   if h: i < i0
   then
     do
-      let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1 (by intlit))
       let slots0 ← vec_index_mut_back (list_t T) slots i list_t.Nil
       hash_map_clear_loop_fwd_back T slots0 i1
   else Result.ret slots
@@ -76,22 +76,22 @@ def hash_map_clear_fwd_back
   do
     let v ←
       hash_map_clear_loop_fwd_back T self.hash_map_slots
-        (USize.ofNatCore 0 (by intlit))
+        (Usize.ofInt 0 (by intlit))
     Result.ret
       {
         self
           with
-          hash_map_num_entries := (USize.ofNatCore 0 (by intlit)),
+          hash_map_num_entries := (Usize.ofInt 0 (by intlit)),
           hash_map_slots := v
       }
 
 /- [hashmap::HashMap::{0}::len] -/
-def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result USize :=
+def hash_map_len_fwd (T : Type) (self : hash_map_t T) : Result Usize :=
   Result.ret self.hash_map_num_entries
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 def hash_map_insert_in_list_loop_fwd
-  (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result Bool) :=
+  (T : Type) (key : Usize) (value : T) (ls : list_t T) : (Result Bool) :=
   match h: ls with
   | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
@@ -104,12 +104,12 @@ decreasing_by hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 def hash_map_insert_in_list_fwd
-  (T : Type) (key : USize) (value : T) (ls : list_t T) : Result Bool :=
+  (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result Bool :=
   hash_map_insert_in_list_loop_fwd T key value ls
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 def hash_map_insert_in_list_loop_back
-  (T : Type) (key : USize) (value : T) (ls : list_t T) : (Result (list_t T)) :=
+  (T : Type) (key : Usize) (value : T) (ls : list_t T) : (Result (list_t T)) :=
   match h: ls with
   | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
@@ -126,25 +126,24 @@ decreasing_by hash_map_insert_in_list_loop_decreases key value ls
 
 /- [hashmap::HashMap::{0}::insert_in_list] -/
 def hash_map_insert_in_list_back
-  (T : Type) (key : USize) (value : T) (ls : list_t T) : Result (list_t T) :=
+  (T : Type) (key : Usize) (value : T) (ls : list_t T) : Result (list_t T) :=
   hash_map_insert_in_list_loop_back T key value ls
 
 /- [hashmap::HashMap::{0}::insert_no_resize] -/
 def hash_map_insert_no_resize_fwd_back
-  (T : Type) (self : hash_map_t T) (key : USize) (value : T) :
+  (T : Type) (self : hash_map_t T) (key : Usize) (value : T) :
   Result (hash_map_t T)
   :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let inserted ← hash_map_insert_in_list_fwd T key value l
     if h: inserted
     then
       do
-        let i0 ← USize.checked_add self.hash_map_num_entries
-          (USize.ofNatCore 1 (by intlit))
+        let i0 ← self.hash_map_num_entries + (Usize.ofInt 1 (by intlit))
         let l0 ← hash_map_insert_in_list_back T key value l
         let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0
         Result.ret
@@ -156,9 +155,9 @@ def hash_map_insert_no_resize_fwd_back
         Result.ret { self with hash_map_slots := v }
 
 /- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result UInt32 :=
-  Result.ret (UInt32.ofNatCore 4294967295 (by intlit))
-def core_num_u32_max_c : UInt32 := eval_global core_num_u32_max_body (by simp)
+def core_num_u32_max_body : Result U32 :=
+  Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
 
 /- [hashmap::HashMap::{0}::move_elements_from_list] -/
 def hash_map_move_elements_from_list_loop_fwd_back
@@ -182,7 +181,7 @@ def hash_map_move_elements_from_list_fwd_back
 
 /- [hashmap::HashMap::{0}::move_elements] -/
 def hash_map_move_elements_loop_fwd_back
-  (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : USize) :
+  (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) :
   (Result ((hash_map_t T) × (Vec (list_t T))))
   :=
   let i0 := vec_len (list_t T) slots
@@ -192,7 +191,7 @@ def hash_map_move_elements_loop_fwd_back
       let l ← vec_index_mut_fwd (list_t T) slots i
       let ls := mem_replace_fwd (list_t T) l list_t.Nil
       let ntable0 ← hash_map_move_elements_from_list_fwd_back T ntable ls
-      let i1 ← USize.checked_add i (USize.ofNatCore 1 (by intlit))
+      let i1 ← i + (Usize.ofInt 1 (by intlit))
       let l0 := mem_replace_back (list_t T) l list_t.Nil
       let slots0 ← vec_index_mut_back (list_t T) slots i l0
       hash_map_move_elements_loop_fwd_back T ntable0 slots0 i1
@@ -203,7 +202,7 @@ decreasing_by hash_map_move_elements_loop_decreases ntable slots i
 
 /- [hashmap::HashMap::{0}::move_elements] -/
 def hash_map_move_elements_fwd_back
-  (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : USize) :
+  (T : Type) (ntable : hash_map_t T) (slots : Vec (list_t T)) (i : Usize) :
   Result ((hash_map_t T) × (Vec (list_t T)))
   :=
   hash_map_move_elements_loop_fwd_back T ntable slots i
@@ -212,19 +211,19 @@ def hash_map_move_elements_fwd_back
 def hash_map_try_resize_fwd_back
   (T : Type) (self : hash_map_t T) : Result (hash_map_t T) :=
   do
-    let max_usize ← scalar_cast USize core_num_u32_max_c
+    let max_usize ← Scalar.cast .Usize core_num_u32_max_c
     let capacity := vec_len (list_t T) self.hash_map_slots
-    let n1 ← USize.checked_div max_usize (USize.ofNatCore 2 (by intlit))
+    let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
     let (i, i0) := self.hash_map_max_load_factor
-    let i1 ← USize.checked_div n1 i
+    let i1 ← n1 / i
     if h: capacity <= i1
     then
       do
-        let i2 ← USize.checked_mul capacity (USize.ofNatCore 2 (by intlit))
+        let i2 ← capacity * (Usize.ofInt 2 (by intlit))
         let ntable ← hash_map_new_with_capacity_fwd T i2 i i0
         let (ntable0, _) ←
           hash_map_move_elements_fwd_back T ntable self.hash_map_slots
-            (USize.ofNatCore 0 (by intlit))
+            (Usize.ofInt 0 (by intlit))
         Result.ret
           {
             ntable0
@@ -236,7 +235,7 @@ def hash_map_try_resize_fwd_back
 
 /- [hashmap::HashMap::{0}::insert] -/
 def hash_map_insert_fwd_back
-  (T : Type) (self : hash_map_t T) (key : USize) (value : T) :
+  (T : Type) (self : hash_map_t T) (key : Usize) (value : T) :
   Result (hash_map_t T)
   :=
   do
@@ -248,7 +247,7 @@ def hash_map_insert_fwd_back
 
 /- [hashmap::HashMap::{0}::contains_key_in_list] -/
 def hash_map_contains_key_in_list_loop_fwd
-  (T : Type) (key : USize) (ls : list_t T) : (Result Bool) :=
+  (T : Type) (key : Usize) (ls : list_t T) : (Result Bool) :=
   match h: ls with
   | list_t.Cons ckey t tl =>
     if h: ckey = key
@@ -261,22 +260,22 @@ decreasing_by hash_map_contains_key_in_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::contains_key_in_list] -/
 def hash_map_contains_key_in_list_fwd
-  (T : Type) (key : USize) (ls : list_t T) : Result Bool :=
+  (T : Type) (key : Usize) (ls : list_t T) : Result Bool :=
   hash_map_contains_key_in_list_loop_fwd T key ls
 
 /- [hashmap::HashMap::{0}::contains_key] -/
 def hash_map_contains_key_fwd
-  (T : Type) (self : hash_map_t T) (key : USize) : Result Bool :=
+  (T : Type) (self : hash_map_t T) (key : Usize) : Result Bool :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod
     hash_map_contains_key_in_list_fwd T key l
 
 /- [hashmap::HashMap::{0}::get_in_list] -/
 def hash_map_get_in_list_loop_fwd
-  (T : Type) (key : USize) (ls : list_t T) : (Result T) :=
+  (T : Type) (key : Usize) (ls : list_t T) : (Result T) :=
   match h: ls with
   | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
@@ -289,22 +288,22 @@ decreasing_by hash_map_get_in_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::get_in_list] -/
 def hash_map_get_in_list_fwd
-  (T : Type) (key : USize) (ls : list_t T) : Result T :=
+  (T : Type) (key : Usize) (ls : list_t T) : Result T :=
   hash_map_get_in_list_loop_fwd T key ls
 
 /- [hashmap::HashMap::{0}::get] -/
 def hash_map_get_fwd
-  (T : Type) (self : hash_map_t T) (key : USize) : Result T :=
+  (T : Type) (self : hash_map_t T) (key : Usize) : Result T :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_fwd (list_t T) self.hash_map_slots hash_mod
     hash_map_get_in_list_fwd T key l
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 def hash_map_get_mut_in_list_loop_fwd
-  (T : Type) (ls : list_t T) (key : USize) : (Result T) :=
+  (T : Type) (ls : list_t T) (key : Usize) : (Result T) :=
   match h: ls with
   | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
@@ -317,12 +316,12 @@ decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 def hash_map_get_mut_in_list_fwd
-  (T : Type) (ls : list_t T) (key : USize) : Result T :=
+  (T : Type) (ls : list_t T) (key : Usize) : Result T :=
   hash_map_get_mut_in_list_loop_fwd T ls key
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 def hash_map_get_mut_in_list_loop_back
-  (T : Type) (ls : list_t T) (key : USize) (ret0 : T) : (Result (list_t T)) :=
+  (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : (Result (list_t T)) :=
   match h: ls with
   | list_t.Cons ckey cvalue tl =>
     if h: ckey = key
@@ -338,28 +337,28 @@ decreasing_by hash_map_get_mut_in_list_loop_decreases ls key
 
 /- [hashmap::HashMap::{0}::get_mut_in_list] -/
 def hash_map_get_mut_in_list_back
-  (T : Type) (ls : list_t T) (key : USize) (ret0 : T) : Result (list_t T) :=
+  (T : Type) (ls : list_t T) (key : Usize) (ret0 : T) : Result (list_t T) :=
   hash_map_get_mut_in_list_loop_back T ls key ret0
 
 /- [hashmap::HashMap::{0}::get_mut] -/
 def hash_map_get_mut_fwd
-  (T : Type) (self : hash_map_t T) (key : USize) : Result T :=
+  (T : Type) (self : hash_map_t T) (key : Usize) : Result T :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     hash_map_get_mut_in_list_fwd T l key
 
 /- [hashmap::HashMap::{0}::get_mut] -/
 def hash_map_get_mut_back
-  (T : Type) (self : hash_map_t T) (key : USize) (ret0 : T) :
+  (T : Type) (self : hash_map_t T) (key : Usize) (ret0 : T) :
   Result (hash_map_t T)
   :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let l0 ← hash_map_get_mut_in_list_back T l key ret0
     let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0
@@ -367,7 +366,7 @@ def hash_map_get_mut_back
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 def hash_map_remove_from_list_loop_fwd
-  (T : Type) (key : USize) (ls : list_t T) : (Result (Option T)) :=
+  (T : Type) (key : Usize) (ls : list_t T) : (Result (Option T)) :=
   match h: ls with
   | list_t.Cons ckey t tl =>
     if h: ckey = key
@@ -385,12 +384,12 @@ decreasing_by hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 def hash_map_remove_from_list_fwd
-  (T : Type) (key : USize) (ls : list_t T) : Result (Option T) :=
+  (T : Type) (key : Usize) (ls : list_t T) : Result (Option T) :=
   hash_map_remove_from_list_loop_fwd T key ls
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 def hash_map_remove_from_list_loop_back
-  (T : Type) (key : USize) (ls : list_t T) : (Result (list_t T)) :=
+  (T : Type) (key : Usize) (ls : list_t T) : (Result (list_t T)) :=
   match h: ls with
   | list_t.Cons ckey t tl =>
     if h: ckey = key
@@ -411,33 +410,32 @@ decreasing_by hash_map_remove_from_list_loop_decreases key ls
 
 /- [hashmap::HashMap::{0}::remove_from_list] -/
 def hash_map_remove_from_list_back
-  (T : Type) (key : USize) (ls : list_t T) : Result (list_t T) :=
+  (T : Type) (key : Usize) (ls : list_t T) : Result (list_t T) :=
   hash_map_remove_from_list_loop_back T key ls
 
 /- [hashmap::HashMap::{0}::remove] -/
 def hash_map_remove_fwd
-  (T : Type) (self : hash_map_t T) (key : USize) : Result (Option T) :=
+  (T : Type) (self : hash_map_t T) (key : Usize) : Result (Option T) :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let x ← hash_map_remove_from_list_fwd T key l
     match h: x with
     | Option.none => Result.ret Option.none
     | Option.some x0 =>
       do
-        let _ ← USize.checked_sub self.hash_map_num_entries
-          (USize.ofNatCore 1 (by intlit))
+        let _ ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit))
         Result.ret (Option.some x0)
 
 /- [hashmap::HashMap::{0}::remove] -/
 def hash_map_remove_back
-  (T : Type) (self : hash_map_t T) (key : USize) : Result (hash_map_t T) :=
+  (T : Type) (self : hash_map_t T) (key : Usize) : Result (hash_map_t T) :=
   do
     let hash ← hash_key_fwd key
     let i := vec_len (list_t T) self.hash_map_slots
-    let hash_mod ← USize.checked_rem hash i
+    let hash_mod ← hash % i
     let l ← vec_index_mut_fwd (list_t T) self.hash_map_slots hash_mod
     let x ← hash_map_remove_from_list_fwd T key l
     match h: x with
@@ -448,8 +446,7 @@ def hash_map_remove_back
         Result.ret { self with hash_map_slots := v }
     | Option.some x0 =>
       do
-        let i0 ← USize.checked_sub self.hash_map_num_entries
-          (USize.ofNatCore 1 (by intlit))
+        let i0 ← self.hash_map_num_entries - (Usize.ofInt 1 (by intlit))
         let l0 ← hash_map_remove_from_list_back T key l
         let v ← vec_index_mut_back (list_t T) self.hash_map_slots hash_mod l0
         Result.ret
@@ -458,65 +455,59 @@ def hash_map_remove_back
 /- [hashmap::test1] -/
 def test1_fwd : Result Unit :=
   do
-    let hm ← hash_map_new_fwd UInt64
+    let hm ← hash_map_new_fwd U64
     let hm0 ←
-      hash_map_insert_fwd_back UInt64 hm (USize.ofNatCore 0 (by intlit))
-        (UInt64.ofNatCore 42 (by intlit))
+      hash_map_insert_fwd_back U64 hm (Usize.ofInt 0 (by intlit))
+        (U64.ofInt 42 (by intlit))
     let hm1 ←
-      hash_map_insert_fwd_back UInt64 hm0 (USize.ofNatCore 128 (by intlit))
-        (UInt64.ofNatCore 18 (by intlit))
+      hash_map_insert_fwd_back U64 hm0 (Usize.ofInt 128 (by intlit))
+        (U64.ofInt 18 (by intlit))
     let hm2 ←
-      hash_map_insert_fwd_back UInt64 hm1 (USize.ofNatCore 1024 (by intlit))
-        (UInt64.ofNatCore 138 (by intlit))
+      hash_map_insert_fwd_back U64 hm1 (Usize.ofInt 1024 (by intlit))
+        (U64.ofInt 138 (by intlit))
     let hm3 ←
-      hash_map_insert_fwd_back UInt64 hm2 (USize.ofNatCore 1056 (by intlit))
-        (UInt64.ofNatCore 256 (by intlit))
-    let i ← hash_map_get_fwd UInt64 hm3 (USize.ofNatCore 128 (by intlit))
-    if h: not (i = (UInt64.ofNatCore 18 (by intlit)))
+      hash_map_insert_fwd_back U64 hm2 (Usize.ofInt 1056 (by intlit))
+        (U64.ofInt 256 (by intlit))
+    let i ← hash_map_get_fwd U64 hm3 (Usize.ofInt 128 (by intlit))
+    if h: not (i = (U64.ofInt 18 (by intlit)))
     then Result.fail Error.panic
     else
       do
         let hm4 ←
-          hash_map_get_mut_back UInt64 hm3 (USize.ofNatCore 1024 (by intlit))
-            (UInt64.ofNatCore 56 (by intlit))
-        let i0 ←
-          hash_map_get_fwd UInt64 hm4 (USize.ofNatCore 1024 (by intlit))
-        if h: not (i0 = (UInt64.ofNatCore 56 (by intlit)))
+          hash_map_get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit))
+            (U64.ofInt 56 (by intlit))
+        let i0 ← hash_map_get_fwd U64 hm4 (Usize.ofInt 1024 (by intlit))
+        if h: not (i0 = (U64.ofInt 56 (by intlit)))
         then Result.fail Error.panic
         else
           do
             let x ←
-              hash_map_remove_fwd UInt64 hm4 (USize.ofNatCore 1024 (by intlit))
+              hash_map_remove_fwd U64 hm4 (Usize.ofInt 1024 (by intlit))
             match h: x with
             | Option.none => Result.fail Error.panic
             | Option.some x0 =>
-              if h: not (x0 = (UInt64.ofNatCore 56 (by intlit)))
+              if h: not (x0 = (U64.ofInt 56 (by intlit)))
               then Result.fail Error.panic
               else
                 do
                   let hm5 ←
-                    hash_map_remove_back UInt64 hm4
-                      (USize.ofNatCore 1024 (by intlit))
+                    hash_map_remove_back U64 hm4 (Usize.ofInt 1024 (by intlit))
                   let i1 ←
-                    hash_map_get_fwd UInt64 hm5 (USize.ofNatCore 0 (by intlit))
-                  if h: not (i1 = (UInt64.ofNatCore 42 (by intlit)))
+                    hash_map_get_fwd U64 hm5 (Usize.ofInt 0 (by intlit))
+                  if h: not (i1 = (U64.ofInt 42 (by intlit)))
                   then Result.fail Error.panic
                   else
                     do
                       let i2 ←
-                        hash_map_get_fwd UInt64 hm5
-                          (USize.ofNatCore 128 (by intlit))
-                      if h: not (i2 = (UInt64.ofNatCore 18 (by intlit)))
+                        hash_map_get_fwd U64 hm5 (Usize.ofInt 128 (by intlit))
+                      if h: not (i2 = (U64.ofInt 18 (by intlit)))
                       then Result.fail Error.panic
                       else
                         do
                           let i3 ←
-                            hash_map_get_fwd UInt64 hm5
-                              (USize.ofNatCore 1056 (by intlit))
-                          if h: not (i3 = (UInt64.ofNatCore 256 (by intlit)))
+                            hash_map_get_fwd U64 hm5
+                              (Usize.ofInt 1056 (by intlit))
+                          if h: not (i3 = (U64.ofInt 256 (by intlit)))
                           then Result.fail Error.panic
                           else Result.ret ()
 
-/- Unit test for [hashmap::test1] -/
-#assert (test1_fwd == .ret ())
-
diff --git a/tests/lean/hashmap/Hashmap/Types.lean b/tests/lean/hashmap/Hashmap/Types.lean
index 9e9e5c03..6eabf7da 100644
--- a/tests/lean/hashmap/Hashmap/Types.lean
+++ b/tests/lean/hashmap/Hashmap/Types.lean
@@ -4,13 +4,13 @@ import Base.Primitives
 
 /- [hashmap::List] -/
 inductive list_t (T : Type) :=
-| Cons : USize -> T -> list_t T -> list_t T
+| Cons : Usize -> T -> list_t T -> list_t T
 | Nil : list_t T
 
 /- [hashmap::HashMap] -/
 structure hash_map_t (T : Type) where
-  hash_map_num_entries : USize
-  hash_map_max_load_factor : (USize × USize)
-  hash_map_max_load : USize
+  hash_map_num_entries : Usize
+  hash_map_max_load_factor : (Usize × Usize)
+  hash_map_max_load : Usize
   hash_map_slots : Vec (list_t T)