Skip to content

Commit

Permalink
remove dead code
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Nov 12, 2023
1 parent 1f8cebd commit 372c47e
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Game/MyNat/LE.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
import Game.MyNat.Multiplication
--import Mathlib.Tactic

namespace MyNat

Expand Down

0 comments on commit 372c47e

Please sign in to comment.