From 42551283ecab981b9bb646cab2e8da5491d71b17 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jul 2023 15:07:09 +0200
Subject: Make minor modifications

---
 tests/lean/Hashmap/Properties.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

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

diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index ee63a065..e1bd8669 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -271,7 +271,8 @@ theorem if_update_eq
   := by
   split <;> simp [Pure.pure]
 
--- TODO: move: small helper
+-- Small helper
+-- TODO: move, and introduce a better solution with nice syntax
 def mk_opaque {α : Sort u} (x : α) : { y : α // y = x}  :=
   ⟨ x, by simp ⟩
 
@@ -328,8 +329,6 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
     else
       simp [*, Pure.pure]
   progress as ⟨ i0 ⟩
-  -- TODO: progress "eager" to match premises with assumptions while instantiating
-  -- meta-variables
   have h_slot : slot_s_inv_hash hm.slots.length (hash_mod_key key hm.slots.length) l.v
     := by
     simp [inv] at hinv
-- 
cgit v1.2.3