Regenerate the test files and fix a proof

33 files changed, 320 insertions, 215 deletions

diff --git a/tests/coq/array/Primitives.v b/tests/coq/array/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/array/Primitives.v
+++ b/tests/coq/array/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 1e457433..cfa1f8fb 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -75,12 +75,6 @@ Definition betree_node_id_counter_fresh_id_back
   Return {| Betree_node_id_counter_next_node_id := i |}
 .
 
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body : result u64 :=
-  Return 18446744073709551615%u64
-.
-Definition core_num_u64_max_c : u64 := core_num_u64_max_body%global.
-
 (** [betree_main::betree::upsert_update]: forward function *)
 Definition betree_upsert_update_fwd
   (prev : option u64) (st : Betree_upsert_fun_state_t) : result u64 :=
@@ -93,8 +87,8 @@ Definition betree_upsert_update_fwd
   | Some prev0 =>
     match st with
     | BetreeUpsertFunStateAdd v =>
-      margin <- u64_sub core_num_u64_max_c prev0;
-      if margin s>= v then u64_add prev0 v else Return core_num_u64_max_c
+      margin <- u64_sub core_u64_max prev0;
+      if margin s>= v then u64_add prev0 v else Return core_u64_max
     | BetreeUpsertFunStateSub v =>
       if prev0 s>= v then u64_sub prev0 v else Return 0%u64
     end
diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/betree/Primitives.v
+++ b/tests/coq/betree/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index e950ba0b..054880d4 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -190,10 +190,6 @@ Definition hash_map_insert_no_resize_fwd_back
       |})
 .
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
 (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hash_map_move_elements_from_list_loop_fwd_back
@@ -259,7 +255,7 @@ Definition hash_map_move_elements_fwd_back
     (there is a single backward function, and the forward function returns ()) *)
 Definition hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hash_map_t T) : result (Hash_map_t T) :=
-  max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+  max_usize <- scalar_cast U32 Usize core_u32_max;
   let capacity := vec_len (List_t T) self.(Hash_map_slots) in
   n1 <- usize_div max_usize 2%usize;
   let (i, i0) := self.(Hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 657d5590..a85adbf2 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -208,10 +208,6 @@ Definition hashmap_hash_map_insert_no_resize_fwd_back
       |})
 .
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 Fixpoint hashmap_hash_map_move_elements_from_list_loop_fwd_back
@@ -282,7 +278,7 @@ Definition hashmap_hash_map_try_resize_fwd_back
   (T : Type) (n : nat) (self : Hashmap_hash_map_t T) :
   result (Hashmap_hash_map_t T)
   :=
-  max_usize <- scalar_cast U32 Usize core_num_u32_max_c;
+  max_usize <- scalar_cast U32 Usize core_u32_max;
   let capacity := vec_len (Hashmap_list_t T) self.(Hashmap_hash_map_slots) in
   n1 <- usize_div max_usize 2%usize;
   let (i, i0) := self.(Hashmap_hash_map_max_load_factor) in
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index f1c32730..5dd78a09 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -12,12 +12,8 @@ Module Constants.
 Definition x0_body : result u32 := Return 0%u32.
 Definition x0_c : u32 := x0_body%global.
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body : result u32 := Return 4294967295%u32.
-Definition core_num_u32_max_c : u32 := core_num_u32_max_body%global.
-
 (** [constants::X1] *)
-Definition x1_body : result u32 := Return core_num_u32_max_c.
+Definition x1_body : result u32 := Return core_u32_max.
 Definition x1_c : u32 := x1_body%global.
 
 (** [constants::X2] *)
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 71a2d9c3..8d6c9c8d 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -394,6 +394,20 @@ Notation "x s< y" := (scalar_ltb x y)  (at level 80) : Primitives_scope.
 Notation "x s>= y" := (scalar_geb x y)  (at level 80) : Primitives_scope.
 Notation "x s> y" := (scalar_gtb x y)  (at level 80) : Primitives_scope.
 
+(** Constants *)
+Definition core_u8_max    := u8_max %u32.
+Definition core_u16_max   := u16_max %u32.
+Definition core_u32_max   := u32_max %u32.
+Definition core_u64_max   := u64_max %u64.
+Definition core_u128_max  := u64_max %u128.
+Axiom core_usize_max : usize. (** TODO *)
+Definition core_i8_max    := i8_max %i32.
+Definition core_i16_max   := i16_max %i32.
+Definition core_i32_max   := i32_max %i32.
+Definition core_i64_max   := i64_max %i64.
+Definition core_i128_max  := i64_max %i128.
+Axiom core_isize_max : isize. (** TODO *)
+
 (*** Range *)
 Record range (T : Type) := mk_range {
   start: T;
diff --git a/tests/fstar/array/Primitives.fst b/tests/fstar/array/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/array/Primitives.fst
+++ b/tests/fstar/array/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 847dc865..2bb2352b 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -60,10 +60,6 @@ let betree_node_id_counter_fresh_id_back
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
   Return { betree_node_id_counter_next_node_id = i }
 
-(** [core::num::u64::{9}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
 (** [betree_main::betree::upsert_update]: forward function *)
 let betree_upsert_update_fwd
   (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -76,8 +72,8 @@ let betree_upsert_update_fwd
   | Some prev0 ->
     begin match st with
     | BetreeUpsertFunStateAdd v ->
-      let* margin = u64_sub core_num_u64_max_c prev0 in
-      if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
+      let* margin = u64_sub core_u64_max prev0 in
+      if margin >= v then u64_add prev0 v else Return core_u64_max
     | BetreeUpsertFunStateSub v ->
       if prev0 >= v then u64_sub prev0 v else Return 0
     end
diff --git a/tests/fstar/betree/Primitives.fst b/tests/fstar/betree/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/betree/Primitives.fst
+++ b/tests/fstar/betree/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 3d08cd3c..8083ee8f 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -60,10 +60,6 @@ let betree_node_id_counter_fresh_id_back
   let* i = u64_add self.betree_node_id_counter_next_node_id 1 in
   Return { betree_node_id_counter_next_node_id = i }
 
-(** [core::num::u64::{9}::MAX] *)
-let core_num_u64_max_body : result u64 = Return 18446744073709551615
-let core_num_u64_max_c : u64 = eval_global core_num_u64_max_body
-
 (** [betree_main::betree::upsert_update]: forward function *)
 let betree_upsert_update_fwd
   (prev : option u64) (st : betree_upsert_fun_state_t) : result u64 =
@@ -76,8 +72,8 @@ let betree_upsert_update_fwd
   | Some prev0 ->
     begin match st with
     | BetreeUpsertFunStateAdd v ->
-      let* margin = u64_sub core_num_u64_max_c prev0 in
-      if margin >= v then u64_add prev0 v else Return core_num_u64_max_c
+      let* margin = u64_sub core_u64_max prev0 in
+      if margin >= v then u64_add prev0 v else Return core_u64_max
     | BetreeUpsertFunStateSub v ->
       if prev0 >= v then u64_sub prev0 v else Return 0
     end
diff --git a/tests/fstar/betree_back_stateful/Primitives.fst b/tests/fstar/betree_back_stateful/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/betree_back_stateful/Primitives.fst
+++ b/tests/fstar/betree_back_stateful/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index f4c13a7b..40cd0477 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -139,10 +139,6 @@ let hash_map_insert_no_resize_fwd_back
     let* v = vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 in
     Return { self with hash_map_slots = v }
 
-(** [core::num::u32::{8}::MAX] *)
-let core_num_u32_max_body : result u32 = Return 4294967295
-let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-
 (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec hash_map_move_elements_from_list_loop_fwd_back
@@ -194,7 +190,7 @@ let hash_map_move_elements_fwd_back
     (there is a single backward function, and the forward function returns ()) *)
 let hash_map_try_resize_fwd_back
   (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
-  let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
+  let* max_usize = scalar_cast U32 Usize core_u32_max in
   let capacity = vec_len (list_t t) self.hash_map_slots in
   let* n1 = usize_div max_usize 2 in
   let (i, i0) = self.hash_map_max_load_factor in
diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 1c94209c..5af90bd8 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -157,10 +157,6 @@ let hashmap_hash_map_insert_no_resize_fwd_back
         hash_mod l0 in
     Return { self with hashmap_hash_map_slots = v }
 
-(** [core::num::u32::{8}::MAX] *)
-let core_num_u32_max_body : result u32 = Return 4294967295
-let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-
 (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
     (there is a single backward function, and the forward function returns ()) *)
 let rec hashmap_hash_map_move_elements_from_list_loop_fwd_back
@@ -218,7 +214,7 @@ let hashmap_hash_map_move_elements_fwd_back
     (there is a single backward function, and the forward function returns ()) *)
 let hashmap_hash_map_try_resize_fwd_back
   (t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
-  let* max_usize = scalar_cast U32 Usize core_num_u32_max_c in
+  let* max_usize = scalar_cast U32 Usize core_u32_max in
   let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
   let* n1 = usize_div max_usize 2 in
   let (i, i0) = self.hashmap_hash_map_max_load_factor in
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_on_disk/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_on_disk/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index d2b0415e..7dfb6f36 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -9,12 +9,8 @@ open Primitives
 let x0_body : result u32 = Return 0
 let x0_c : u32 = eval_global x0_body
 
-(** [core::num::u32::{8}::MAX] *)
-let core_num_u32_max_body : result u32 = Return 4294967295
-let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-
 (** [constants::X1] *)
-let x1_body : result u32 = Return core_num_u32_max_c
+let x1_body : result u32 = Return core_u32_max
 let x1_c : u32 = eval_global x1_body
 
 (** [constants::X2] *)
diff --git a/tests/fstar/misc/Primitives.fst b/tests/fstar/misc/Primitives.fst
index 9db82069..cd18cf29 100644
--- a/tests/fstar/misc/Primitives.fst
+++ b/tests/fstar/misc/Primitives.fst
@@ -169,17 +169,44 @@ let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) :
 
 /// The scalar types
 type isize : eqtype = scalar Isize
-type i8 : eqtype = scalar I8
-type i16 : eqtype = scalar I16
-type i32 : eqtype = scalar I32
-type i64 : eqtype = scalar I64
-type i128 : eqtype = scalar I128
+type i8    : eqtype = scalar I8
+type i16   : eqtype = scalar I16
+type i32   : eqtype = scalar I32
+type i64   : eqtype = scalar I64
+type i128  : eqtype = scalar I128
 type usize : eqtype = scalar Usize
-type u8 : eqtype = scalar U8
-type u16 : eqtype = scalar U16
-type u32 : eqtype = scalar U32
-type u64 : eqtype = scalar U64
-type u128 : eqtype = scalar U128
+type u8    : eqtype = scalar U8
+type u16   : eqtype = scalar U16
+type u32   : eqtype = scalar U32
+type u64   : eqtype = scalar U64
+type u128  : eqtype = scalar U128
+
+
+let core_isize_min : isize = isize_min
+let core_isize_max : isize = isize_max
+let core_i8_min    : i8 = i8_min
+let core_i8_max    : i8 = i8_max
+let core_i16_min   : i16 = i16_min
+let core_i16_max   : i16 = i16_max
+let core_i32_min   : i32 = i32_min
+let core_i32_max   : i32 = i32_max
+let core_i64_min   : i64 = i64_min
+let core_i64_max   : i64 = i64_max
+let core_i128_min  : i128 = i128_min
+let core_i128_max  : i128 = i128_max
+
+let core_usize_min : usize = usize_min
+let core_usize_max : usize = usize_max
+let core_u8_min    : u8 = u8_min
+let core_u8_max    : u8 = u8_max
+let core_u16_min   : u16 = u16_min
+let core_u16_max   : u16 = u16_max
+let core_u32_min   : u32 = u32_min
+let core_u32_max   : u32 = u32_max
+let core_u64_min   : u64 = u64_min
+let core_u64_max   : u64 = u64_max
+let core_u128_min  : u128 = u128_min
+let core_u128_max  : u128 = u128_max
 
 /// Negation
 let isize_neg = scalar_neg #Isize
diff --git a/tests/hol4/betree/betreeMain_FunsScript.sml b/tests/hol4/betree/betreeMain_FunsScript.sml
index 5e604f8c..bd16c16c 100644
--- a/tests/hol4/betree/betreeMain_FunsScript.sml
+++ b/tests/hol4/betree/betreeMain_FunsScript.sml
@@ -88,14 +88,6 @@ val betree_node_id_counter_fresh_id_back_def = Define ‘
     od
 ’
 
-(** [core::num::u64::{9}::MAX] *)
-Definition core_num_u64_max_body_def:
-  core_num_u64_max_body : u64 result = Return (int_to_u64 18446744073709551615)
-End
-Definition core_num_u64_max_c_def:
-  core_num_u64_max_c : u64 = get_return_value core_num_u64_max_body
-End
-
 val betree_upsert_update_fwd_def = Define ‘
   (** [betree_main::betree::upsert_update]: forward function *)
   betree_upsert_update_fwd
@@ -109,8 +101,8 @@ val betree_upsert_update_fwd_def = Define ‘
       (case st of
       | BetreeUpsertFunStateAdd v =>
         do
-        margin <- u64_sub core_num_u64_max_c prev0;
-        if u64_ge margin v then u64_add prev0 v else Return core_num_u64_max_c
+        margin <- u64_sub core_u64_max prev0;
+        if u64_ge margin v then u64_add prev0 v else Return core_u64_max
         od
       | BetreeUpsertFunStateSub v =>
         if u64_ge prev0 v then u64_sub prev0 v else Return (int_to_u64 0)))
diff --git a/tests/hol4/betree/betreeMain_FunsTheory.sig b/tests/hol4/betree/betreeMain_FunsTheory.sig
index 6c249f70..c922ca9f 100644
--- a/tests/hol4/betree/betreeMain_FunsTheory.sig
+++ b/tests/hol4/betree/betreeMain_FunsTheory.sig
@@ -58,8 +58,6 @@ sig
     val betree_store_internal_node_fwd_def : thm
     val betree_store_leaf_node_fwd_def : thm
     val betree_upsert_update_fwd_def : thm
-    val core_num_u64_max_body_def : thm
-    val core_num_u64_max_c_def : thm
     val main_fwd_def : thm
   
   val betreeMain_Funs_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1215,22 +1213,14 @@ sig
             case st of
               BetreeUpsertFunStateAdd v =>
                 do
-                  margin <- u64_sub core_num_u64_max_c prev0;
+                  margin <- u64_sub core_u64_max prev0;
                   if u64_ge margin v then u64_add prev0 v
-                  else Return core_num_u64_max_c
+                  else Return core_u64_max
                 od
             | BetreeUpsertFunStateSub v' =>
               if u64_ge prev0 v' then u64_sub prev0 v'
               else Return (int_to_u64 0)
    
-   [core_num_u64_max_body_def]  Definition
-      
-      ⊢ core_num_u64_max_body = Return (int_to_u64 18446744073709551615)
-   
-   [core_num_u64_max_c_def]  Definition
-      
-      ⊢ core_num_u64_max_c = get_return_value core_num_u64_max_body
-   
    [main_fwd_def]  Definition
       
       ⊢ main_fwd = Return ()
diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
index e3c3d2a5..682c5760 100644
--- a/tests/hol4/hashmap/hashmap_FunsScript.sml
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -170,14 +170,6 @@ val hash_map_insert_no_resize_fwd_back_def = Define ‘
     od
 ’
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
   (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
       (there is a single backward function, and the forward function returns ()) *)
@@ -241,7 +233,7 @@ val hash_map_try_resize_fwd_back_def = Define ‘
       (there is a single backward function, and the forward function returns ()) *)
   hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
     do
-    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    max_usize <- mk_usize (u32_to_int core_u32_max);
     let capacity = vec_len self.hash_map_slots in
     do
     n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap/hashmap_FunsTheory.sig b/tests/hol4/hashmap/hashmap_FunsTheory.sig
index 50482547..bb3e192b 100644
--- a/tests/hol4/hashmap/hashmap_FunsTheory.sig
+++ b/tests/hol4/hashmap/hashmap_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
   type thm = Thm.thm
   
   (*  Definitions  *)
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val hash_key_fwd_def : thm
     val hash_map_allocate_slots_fwd_def : thm
     val hash_map_allocate_slots_loop_fwd_def : thm
@@ -48,14 +46,6 @@ sig
 (*
    [hashmap_Types] Parent theory of "hashmap_Funs"
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [hash_key_fwd_def]  Definition
       
       ⊢ ∀k. hash_key_fwd k = Return k
@@ -472,7 +462,7 @@ sig
       ⊢ ∀self.
           hash_map_try_resize_fwd_back self =
           do
-            max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+            max_usize <- mk_usize (u32_to_int core_u32_max);
             capacity <<- vec_len self.hash_map_slots;
             n1 <- usize_div max_usize (int_to_usize 2);
             (i,i0) <<- self.hash_map_max_load_factor;
diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 7259f2f5..8bc12fa5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1296,7 +1296,7 @@ Proof
   rw [hash_map_try_resize_fwd_back_def] >>
   (* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *)
   assume_tac usize_u32_bounds >>
-  fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >>
+  fs [core_u32_max_def, u32_max_def] >>
   massage >> fs [mk_usize_def, u32_max_def] >>
   (* / 2 *)
   progress >>
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
index b21c4f58..c1e30aa6 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
@@ -193,14 +193,6 @@ val hashmap_hash_map_insert_no_resize_fwd_back_def = Define ‘
     od
 ’
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 val [hashmap_hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
   (** [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
       (there is a single backward function, and the forward function returns ()) *)
@@ -271,7 +263,7 @@ val hashmap_hash_map_try_resize_fwd_back_def = Define ‘
   hashmap_hash_map_try_resize_fwd_back
     (self : 't hashmap_hash_map_t) : 't hashmap_hash_map_t result =
     do
-    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    max_usize <- mk_usize (u32_to_int core_u32_max);
     let capacity = vec_len self.hashmap_hash_map_slots in
     do
     n1 <- usize_div max_usize (int_to_usize 2);
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
index 1d24cb26..d4e43d9a 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
@@ -3,8 +3,6 @@ sig
   type thm = Thm.thm
   
   (*  Definitions  *)
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val hashmap_hash_key_fwd_def : thm
     val hashmap_hash_map_allocate_slots_fwd_def : thm
     val hashmap_hash_map_allocate_slots_loop_fwd_def : thm
@@ -50,14 +48,6 @@ sig
 (*
    [hashmapMain_Opaque] Parent theory of "hashmapMain_Funs"
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [hashmap_hash_key_fwd_def]  Definition
       
       ⊢ ∀k. hashmap_hash_key_fwd k = Return k
@@ -506,7 +496,7 @@ sig
       ⊢ ∀self.
           hashmap_hash_map_try_resize_fwd_back self =
           do
-            max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+            max_usize <- mk_usize (u32_to_int core_u32_max);
             capacity <<- vec_len self.hashmap_hash_map_slots;
             n1 <- usize_div max_usize (int_to_usize 2);
             (i,i0) <<- self.hashmap_hash_map_max_load_factor;
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/misc-constants/constantsScript.sml
index d589d348..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/misc-constants/constantsScript.sml
@@ -13,17 +13,9 @@ Definition x0_c_def:
   x0_c : u32 = get_return_value x0_body
 End
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 (** [constants::X1] *)
 Definition x1_body_def:
-  x1_body : u32 result = Return core_num_u32_max_c
+  x1_body : u32 result = Return core_u32_max
 End
 Definition x1_c_def:
   x1_c : u32 = get_return_value x1_body
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 149d7e22..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -4,8 +4,6 @@ sig
   
   (*  Definitions  *)
     val add_fwd_def : thm
-    val core_num_u32_max_body_def : thm
-    val core_num_u32_max_c_def : thm
     val get_z1_fwd_def : thm
     val get_z1_z1_body_def : thm
     val get_z1_z1_c_def : thm
@@ -110,14 +108,6 @@ sig
       
       ⊢ ∀a b. add_fwd a b = i32_add a b
    
-   [core_num_u32_max_body_def]  Definition
-      
-      ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-   
-   [core_num_u32_max_c_def]  Definition
-      
-      ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-   
    [get_z1_fwd_def]  Definition
       
       ⊢ get_z1_fwd = Return get_z1_z1_c
@@ -321,7 +311,7 @@ sig
    
    [x1_body_def]  Definition
       
-      ⊢ x1_body = Return core_num_u32_max_c
+      ⊢ x1_body = Return core_u32_max
    
    [x1_c_def]  Definition
       
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 07ef08dc..6681731f 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -64,11 +64,6 @@ def betree.NodeIdCounter.fresh_id_back
     let i ← self.next_node_id + (U64.ofInt 1)
     Result.ret { next_node_id := i }
 
-/- [core::num::u64::{9}::MAX] -/
-def core_num_u64_max_body : Result U64 :=
-  Result.ret (U64.ofInt 18446744073709551615)
-def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
-
 /- [betree_main::betree::upsert_update]: forward function -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -81,10 +76,10 @@ def betree.upsert_update
     match st with
     | betree.UpsertFunState.Add v =>
       do
-        let margin ← core_num_u64_max_c - prev0
+        let margin ← core_u64_max - prev0
         if margin >= v
         then prev0 + v
-        else Result.ret core_num_u64_max_c
+        else Result.ret core_u64_max
     | betree.UpsertFunState.Sub v =>
       if prev0 >= v
       then prev0 - v
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 51b415d6..b0cdaa90 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -9,12 +9,8 @@ namespace constants
 def x0_body : Result U32 := Result.ret (U32.ofInt 0)
 def x0_c : U32 := eval_global x0_body (by simp)
 
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
 /- [constants::X1] -/
-def x1_body : Result U32 := Result.ret core_num_u32_max_c
+def x1_body : Result U32 := Result.ret core_u32_max
 def x1_c : U32 := eval_global x1_body (by simp)
 
 /- [constants::X2] -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 30b30e0b..01c61de4 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -132,10 +132,6 @@ def HashMap.insert_no_resize
         let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
         Result.ret { self with slots := v }
 
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
 /- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def HashMap.move_elements_from_list_loop
@@ -184,7 +180,7 @@ def HashMap.move_elements
    (there is a single backward function, and the forward function returns ()) -/
 def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-    let max_usize ← Scalar.cast .Usize core_num_u32_max_c
+    let max_usize ← Scalar.cast .Usize core_u32_max
     let capacity := Vec.len (List T) self.slots
     let n1 ← max_usize / (Usize.ofInt 2)
     let (i, i0) := self.max_load_factor
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index aec957ec..848b1a35 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -147,10 +147,6 @@ def hashmap.HashMap.insert_no_resize
         let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
         Result.ret { self with slots := v }
 
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
 /- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
    (there is a single backward function, and the forward function returns ()) -/
 divergent def hashmap.HashMap.move_elements_from_list_loop
@@ -206,7 +202,7 @@ def hashmap.HashMap.move_elements
 def hashmap.HashMap.try_resize
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
-    let max_usize ← Scalar.cast .Usize core_num_u32_max_c
+    let max_usize ← Scalar.cast .Usize core_u32_max
     let capacity := Vec.len (hashmap.List T) self.slots
     let n1 ← max_usize / (Usize.ofInt 2)
     let (i, i0) := self.max_load_factor