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/lean/HashmapMain/Funs.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'tests/lean/HashmapMain')

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