From 65a77968d0abc2d01da92aa8982256855e7519a6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 5 Apr 2024 14:04:25 +0200
Subject: Update the lean toolchain and fix the proofs

---
 backends/lean/Base/Arith/Int.lean | 1 -
 1 file changed, 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 a57f8bb1..5a85dff0 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,7 +3,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 -- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
 --import Mathlib.Tactic.Omega
-- 
cgit v1.2.3