From 03492250b45855fe9db5e0a28a96166607cd84a1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 14:14:34 +0200
Subject: Make some proofs in Hashmap/Properties.lean and improve progress

---
 backends/lean/Base/Arith/Int.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Arith')

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
-- 
cgit v1.2.3