summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
authorSon Ho2024-06-12 14:45:58 +0200
committerSon Ho2024-06-12 14:45:58 +0200
commit7763a8ef8d5190fad39e9e677c5f44c536973655 (patch)
treed7ec59a3658f46e9c580b3bd39774a27250e0052 /backends/lean/Base/Progress
parente60d525fe3dffa035d2a551af624747dca6e1c1e (diff)
Add the Simp.Config to the simp wrappers
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Progress.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index f2a56e50..39a48044 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -135,7 +135,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
Tactic.focus do
let _ ←
tryTac
- (simpAt true []
+ (simpAt true {} []
[``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
-- It may happen that at this point the goal is already solved (though this is rare)
@@ -144,7 +144,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
else
trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}"
-- TODO: remove this (some types get unfolded too much: we "fold" them back)
- let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
+ let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep)
trace[Progress] "goal after folding back scalar types: {← getMainGoal}"
-- Clear the equality, unless the user requests not to do so
let mgoal ← do