From 112685b5244b1bcde13d7a13e3d44cc8851de49b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 10 Feb 2022 13:34:30 +0100
Subject: Make progress on the proofs of HashMap

---
 fstar/Primitives.fst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'fstar/Primitives.fst')

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
@@ -240,9 +243,6 @@ type vec (a : Type0) = v:list a{length v <= usize_max}
 let vec_new (a  : Type0) : vec a = assert_norm(length #a [] == 0); []
 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) :
-- 
cgit v1.2.3