chore: add a dummy `evalTactic try simp_mem

leanprover · Sep 25, 2024 · e1239bd · e1239bd
1 parent e4bf48b
commit e1239bd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
@@ -330,6 +330,8 @@ since that would be way too expensive.
 -/
 def simpMem (_c : SymContext) (mvar : MVarId) : TacticM MVarId := do 
   /-
+  This should actually allow us to not need the follow processing in `Proofs/Popcount32`:
+
   simp only [←Memory.mem_eq_iff_read_mem_bytes_eq] at *
   simp only [memory_rules] at *
   intro n addr h_separate