Skip to content

Commit

Permalink
Remove outdated import
Browse files Browse the repository at this point in the history
  • Loading branch information
tomaz1502 committed Dec 17, 2024
1 parent 6d12bef commit 0901b50
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions Smt/Reconstruct/Int/Core.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 0901b50

Please sign in to comment.