diff options
| author | Son Ho | 2023-07-12 15:41:29 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-12 15:41:29 +0200 |
| commit | 59e4a06480b5365f48dc68de80f44841f94094ed (patch) | |
| tree | 00644dda183bff958381183939f4eb54d97ed242 /backends/lean/Base/Progress | |
| parent | a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 (diff) | |
Improve the handling of arithmetic bounds
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 5 |
1 files changed, 3 insertions, 2 deletions
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!] |