From 59e4a06480b5365f48dc68de80f44841f94094ed Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 15:41:29 +0200
Subject: Improve the handling of arithmetic bounds

---
 backends/lean/Base/Progress/Progress.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Progress/Progress.lean')

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 4c68b3bd..a4df5c96 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -92,9 +92,10 @@ def progressLookupTheorem (asmTac : TacticM Unit) : TacticM Unit := do
       if ← isConj (← inferType h) then
         splitConjTac h (fun h _ => k h)
       else k h
-    -- Simplify the target by using the equality
+    -- Simplify the target by using the equality and some monad simplifications
     splitConj fun h => do
-    simpAt [] [] [h.fvarId!] (.targets #[] true)
+    simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+           [h.fvarId!] (.targets #[] true)
     -- Clear the equality
     let mgoal ← getMainGoal
     let mgoal ← mgoal.tryClearMany #[h.fvarId!]
-- 
cgit v1.2.3