From d2030538caf01bac4aa06c312bd4d8b1cbd3c6ea Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 12 Feb 2022 11:53:57 +0100
Subject: Make minor modifications to Hashmap.Properties.fst

---
 tests/hashmap/Hashmap.Properties.fst | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index 577398fd..a27ee34a 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -1391,16 +1391,20 @@ let hash_map_insert_no_resize_s_get_diff_lem #t hm key value key' =
 
 (*** move_elements_from_list *)
 
-type hash_map_slots_s_res (t : Type0) = res:result (hash_map_slots_s t){
-    match res with
-    | Fail -> True
-    | Return hm -> is_pos_usize (length hm)
-  }
-
 let rec hash_map_move_elements_from_list_s
-  (#t : Type0) (hm : hash_map_slots_s t{is_pos_usize (length hm)})
+  (#t : Type0) (hm : hash_map_slots_s_nes t)
   (ls : slot_s t) :
-  Tot (hash_map_slots_s_res t) (decreases ls) =
+  Pure (result (hash_map_slots_s t))
+  (requires (True))
+  (ensures (fun res ->
+    // Having a great time here: if we use `result (hash_map_slots_s_res t)`
+    // as the return type, instead of having this awkward match, the proof
+    // of [hash_map_move_elements_fwd_back_lem] fails. I guess it comes from
+    // F*'s poor subtyping.
+    match res with
+    | Fail -> True
+    | Return hm -> is_pos_usize (length hm)))
+  (decreases ls) =
   match ls with
   | [] -> Return hm
   | (key, value) :: ls' ->
-- 
cgit v1.2.3