From 67fb76ae5801fdb8f134394425e466dbe611a54b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 27 Oct 2023 12:26:20 +0200
Subject: Regenerate more F* files

---
 tests/fstar/hashmap/Primitives.fst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tests/fstar/hashmap')

diff --git a/tests/fstar/hashmap/Primitives.fst b/tests/fstar/hashmap/Primitives.fst
index 3110b247..71d75c11 100644
--- a/tests/fstar/hashmap/Primitives.fst
+++ b/tests/fstar/hashmap/Primitives.fst
@@ -707,5 +707,7 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (t idx : Type0)
 let alloc_vec_Vec_index_mut_back_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) (x : a) :
   Lemma (
     alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x ==
-      alloc_vec_Vec_update_usize v i x) =
+      alloc_vec_Vec_update_usize v i x)
+  [SMTPat (alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x)]
+  =
   admit()
-- 
cgit v1.2.3