From 0901b5084934d4e9cbdd7707f0c30b522149f7e0 Mon Sep 17 00:00:00 2001 From: tomaz1502 Date: Tue, 17 Dec 2024 13:33:09 -0300 Subject: [PATCH] Remove outdated import --- Smt/Reconstruct/Int/Core.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Smt/Reconstruct/Int/Core.lean b/Smt/Reconstruct/Int/Core.lean index e0b3395e..aedd6eb1 100644 --- a/Smt/Reconstruct/Int/Core.lean +++ b/Smt/Reconstruct/Int/Core.lean @@ -5,10 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas, Abdalrhman Mohamed -/ -import Batteries.Data.Int - - - namespace Int @[simp] protected theorem natCast_eq_zero {n : Nat} : (n : Int) = 0 ↔ n = 0 := by