Skip to content

Commit

Permalink
remove excessive import
Browse files Browse the repository at this point in the history
kbuzzard committed Nov 12, 2023
1 parent f33eb30 commit 03d7490
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Game/MyNat/Definition.lean
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import Game.Tactic.LabelAttr
import Mathlib.Tactic
import Game.Tactic.LabelAttr -- MyNat_decide attribute

/-- Our copy of the natural numbers called `MyNat`, with notation `ℕ`. -/
inductive MyNat where
| zero : MyNat

0 comments on commit 03d7490

Please sign in to comment.