diff options
| author | Son Ho | 2023-09-13 07:33:30 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-13 07:33:30 +0200 |
| commit | 78a2731924aa13989998c6be4a5a6865ce5098aa (patch) | |
| tree | 7e641855fc8b943bd7ea3a314bab3d8a275afde3 /tests/lean/Hashmap/Properties.lean | |
| parent | 5921be8e2e8955db5101354d8bf29ae6a3693f48 (diff) | |
Make minor modifications
Diffstat (limited to 'tests/lean/Hashmap/Properties.lean')
| -rw-r--r-- | tests/lean/Hashmap/Properties.lean | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index ab95b854..6bc821d3 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -303,19 +303,17 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] simp only [hash_key, bind_tc_ret] -- TODO: annoying - have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint + have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by intro simp_all [inv] - progress keep _ as ⟨ hash_mod, hhm ⟩ - have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac + progress as ⟨ hash_mod, hhm ⟩ + have _ : 0 ≤ hash_mod.val := by scalar_tac have _ : hash_mod.val < Vec.length hm.slots := by have : 0 < hm.slots.val.len := by simp [inv] at hinv simp [hinv] -- TODO: we want to automate that simp [*, Int.emod_lt_of_pos] - -- TODO: change the spec of Vec.index_mut to introduce a let-binding. - -- or: make progress introduce the let-binding by itself (this is clearer) progress as ⟨ l, h_leq ⟩ -- TODO: make progress use the names written in the goal progress as ⟨ inserted ⟩ |