From fab63abb07bcd1f1c28c5be386549185b4139003 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 13 Feb 2022 22:30:07 +0100
Subject: Make progress on map_s

---
 tests/hashmap/Hashmap.Properties.fst | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'tests/hashmap/Hashmap.Properties.fst')

diff --git a/tests/hashmap/Hashmap.Properties.fst b/tests/hashmap/Hashmap.Properties.fst
index b8788c8c..099fd2c6 100644
--- a/tests/hashmap/Hashmap.Properties.fst
+++ b/tests/hashmap/Hashmap.Properties.fst
@@ -464,6 +464,7 @@ let slots_t_al_v (#t : Type0) (slots : slots_t t) : assoc_list t =
 /// lemmas shown to the user.
 type hash_map_s t = list (slot_s t)
 
+// TODO: why not always have the condition on the length?
 // 'nes': "non-empty slots"
 type hash_map_s_nes (t : Type0) : Type0 =
   hm:hash_map_s t{is_pos_usize (length hm)}
@@ -616,6 +617,7 @@ type map_s (t : Type0) = {
   max_load_divis : usize;
 }
 
+(*
 val to_v (#t : Type0) (hm : hash_map_t t) : map_s t
 let to_v #t hm =
   let slots = hash_map_t_v hm in
@@ -629,6 +631,10 @@ let to_v #t hm =
 val len_s (#t : Type0) (m : map_s t) : nat
 let len_s #t m = hash_map_s_len m.slots
 
+val find_s (#t : Type0) (m : map_s t) (k : key) : option t
+let find_s #t m k = hash_map_s_find m.slots k
+*)
+
 let map_s_max_load (#t : Type0) (m : map_s t{m.max_load_divis > 0}) : nat =
   let capacity = length m.slots in
   let dividend = m.max_load_divid in
-- 
cgit v1.2.3