diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index a2fa0d7d..29b5834b 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -165,8 +165,7 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) ( have : distinct_keys (AList.v tl0) := by simp [distinct_keys] at hdk simp [hdk, distinct_keys] - progress keep heq as ⟨ b, tl1 .. ⟩ - simp only [insert_in_list] at heq + progress as ⟨ b, tl1 .. ⟩ have : slot_s_inv_hash l (hash_mod_key key l) (AList.v (AList.Cons k v tl1)) := by simp [AList.v, slot_s_inv_hash] at * simp [*] |