diff options
| author | Son Ho | 2024-06-17 07:15:26 +0200 |
|---|---|---|
| committer | Son Ho | 2024-06-17 07:15:26 +0200 |
| commit | 1021cdea98043dd935dbc8dbe633b90fda68047d (patch) | |
| tree | dc2f420cf5167690da9dfebe358ba56bf05e1b1e /tests/lean/Hashmap/Properties.lean | |
| parent | f4739fba4be95818ca01776837c8d610e443a45b (diff) | |
Update the tests
Diffstat (limited to 'tests/lean/Hashmap/Properties.lean')
| -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 [*] |