Make progress on the proofs of HashMap

1 files changed, 4 insertions, 4 deletions

diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index fbf8140a..4642d080 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -7,7 +7,10 @@ open FStar.List.Tot
 
 (*** Utilities *)
 val list_update (#a : Type0) (ls : list a) (i : nat{i < length ls}) (x : a) :
-  ls':list a{length ls' = length ls}
+  ls':list a{
+    length ls' = length ls /\
+    index ls' i == x
+  }
 #push-options "--fuel 1"
 let rec list_update #a ls i x =
   match ls with
@@ -242,9 +245,6 @@ let vec_len (a : Type0) (v : vec a) : usize = length v
 
 // The **forward** function shouldn't be used
 let vec_push_fwd (a  : Type0) (v : vec a) (x : a) : unit = ()
-
-// The **forward** function shouldn't be used
-let vec_push_fwd (a  : Type0) (v : vec a) (x : a) : unit = ()
 let vec_push_back (a  : Type0) (v : vec a) (x : a) :
   Pure (result (vec a))
   (requires True)