summaryrefslogtreecommitdiff
path: root/tests/lean/HashmapMain/Funs.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/HashmapMain/Funs.lean')
-rw-r--r--tests/lean/HashmapMain/Funs.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index ea28b03f..74fe8a54 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -261,7 +261,7 @@ def hashmap.HashMap.contains_key
let hash ← hashmap.hash_key key
let i := Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index (hashmap.List T) self.slots hash_mod
+ let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod
hashmap.HashMap.contains_key_in_list T key l
/- [hashmap_main::hashmap::HashMap::{0}::get_in_list]: loop 0: forward function -/
@@ -286,7 +286,7 @@ def hashmap.HashMap.get
let hash ← hashmap.hash_key key
let i := Vec.len (hashmap.List T) self.slots
let hash_mod ← hash % i
- let l ← Vec.index (hashmap.List T) self.slots hash_mod
+ let l ← Vec.index_shared (hashmap.List T) self.slots hash_mod
hashmap.HashMap.get_in_list T key l
/- [hashmap_main::hashmap::HashMap::{0}::get_mut_in_list]: loop 0: forward function -/