From c656688ff4895904b4bb5e2f89037f1e75c9fa00 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Aug 2023 20:02:37 +0200
Subject: Make minor modifications

---
 tests/lean/Hashmap/Funs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/Hashmap/Funs.lean')

diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 2fa981ce..d6796932 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -239,7 +239,7 @@ def HashMap.contains_key
     let hash ← hash_key key
     let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (List T) self.slots hash_mod
+    let l ← Vec.index_shared (List T) self.slots hash_mod
     HashMap.contains_key_in_list T key l
 
 /- [hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/
@@ -262,7 +262,7 @@ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
     let hash ← hash_key key
     let i := Vec.len (List T) self.slots
     let hash_mod ← hash % i
-    let l ← Vec.index (List T) self.slots hash_mod
+    let l ← Vec.index_shared (List T) self.slots hash_mod
     HashMap.get_in_list T key l
 
 /- [hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/
-- 
cgit v1.2.3