From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/hashmap/hashmap_FunsTheory.sig | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'tests/hol4/hashmap/hashmap_FunsTheory.sig')

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;
-- 
cgit v1.2.3