chore(data/nat/enat): move into a subfolder (#17106)

I'm going to add more files about `enat` soon.
leanprover-community · Oct 22, 2022 · 8005d57 · 8005d57
1 parent 5bff97f
commit 8005d57
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 3 deletions.
diff --git a/src/analysis/calculus/cont_diff.lean b/src/analysis/calculus/cont_diff.lean
@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.mean_value
 import analysis.normed_space.multilinear
 import analysis.calculus.formal_multilinear_series
-import data.nat.enat
+import data.enat.basic
 import tactic.congrm
 
 /-!

diff --git a/src/data/nat/enat.lean → src/data/enat/basic.lean b/src/data/nat/enat.lean → src/data/enat/basic.lean
diff --git a/src/data/nat/part_enat.lean b/src/data/nat/part_enat.lean
@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import algebra.hom.equiv
 import data.part
-import data.nat.enat
+import data.enat.basic
 import tactic.norm_num
 
 /-!

diff --git a/src/data/polynomial/degree/trailing_degree.lean b/src/data/polynomial/degree/trailing_degree.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.nat.enat
+import data.enat.basic
 import data.polynomial.degree.definitions
 
 /-!