summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Arith')
-rw-r--r--backends/lean/Base/Arith/Int.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index ac011998..fa957293 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -198,7 +198,7 @@ def intTac (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM Unit := do
-- Split the conjunctions in the goal
Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-- Call linarith
- let linarith :=
+ let linarith := do
let cfg : Linarith.LinarithConfig := {
-- We do this with our custom preprocessing
splitNe := false