Merge branch 'main' into simp-mem-mem-omega-3

leanprover · Oct 30, 2024 · e2daf44 · e2daf44
2 parents 617e32b + 25fffe0
commit e2daf44
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Arm/Memory/Common.lean b/Arm/Memory/Common.lean
@@ -290,7 +290,6 @@ def omega (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs
     TacticM.withTraceNode' m!"goal post `bv_toNat` reductions (Note: can be large)" do
       trace[simp_mem.info] "{goal}"
     -- @bollu: TODO: understand what precisely we are recovering from.
-    -- | TODO: replace with bvOmegaBench, and make THAT work in TacticM.
     withoutRecover do
       evalTactic (← `(tactic| bv_omega_bench))