Skip to content

Commit 0f79c0c

Browse files
jcommelinjcommelin
committed
chore(Data/Nat/Notation): move Init/Data/Nat/Notation (#14761)
1 parent f1a20a0 commit 0f79c0c

21 files changed

+30
-41
lines changed

‎Mathlib.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -2268,6 +2268,7 @@ import Mathlib.Data.Nat.Log
22682268
import Mathlib.Data.Nat.MaxPowDiv
22692269
import Mathlib.Data.Nat.ModEq
22702270
import Mathlib.Data.Nat.Multiplicity
2271+
import Mathlib.Data.Nat.Notation
22712272
import Mathlib.Data.Nat.Nth
22722273
import Mathlib.Data.Nat.Order.Lemmas
22732274
import Mathlib.Data.Nat.PSub
@@ -2731,7 +2732,6 @@ import Mathlib.Init.Data.Nat.Basic
27312732
import Mathlib.Init.Data.Nat.Div
27322733
import Mathlib.Init.Data.Nat.GCD
27332734
import Mathlib.Init.Data.Nat.Lemmas
2734-
import Mathlib.Init.Data.Nat.Notation
27352735
import Mathlib.Init.Data.Option.Basic
27362736
import Mathlib.Init.Data.Option.Init.Lemmas
27372737
import Mathlib.Init.Data.Option.Lemmas

‎Mathlib/Data/Fin/Fin2.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Mathport.Rename
88
import Mathlib.Data.Fintype.Basic
99
import Mathlib.Logic.Function.Basic

‎Mathlib/Data/List/Defs.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2014 Parikshit Khanna. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Control.Functor
88
import Mathlib.Data.SProd
99
import Mathlib.Util.CompileInductive

‎Mathlib/Data/Nat/Notation.lean

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
/-
2+
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Floris van Doorn, Leonardo de Moura
5+
-/
6+
7+
/-!
8+
# Notation `ℕ` for the natural numbers.
9+
-/
10+
11+
@[inherit_doc] notation "ℕ" => Nat

‎Mathlib/Data/Rat/Init.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johannes Hölzl, Mario Carneiro, Yaël Dillies
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Mathport.Rename
88
import Mathlib.Tactic.Lemma
99
import Mathlib.Tactic.ProjectionNotation

‎Mathlib/Data/Stream/Defs.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Leonardo de Moura
55
-/
66
import Mathlib.Mathport.Rename
7-
import Mathlib.Init.Data.Nat.Notation
7+
import Mathlib.Data.Nat.Notation
88

99
#align_import data.stream.defs from "leanprover-community/mathlib"@"39af7d3bf61a98e928812dbc3e16f4ea8b795ca3"
1010

‎Mathlib/Data/String/Lemmas.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2021 Chris Bailey. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Bailey
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Data.String.Defs
88
import Mathlib.Tactic.Basic
99

‎Mathlib/Data/Tree/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Wojciech Nawrocki
55
-/
66
import Batteries.Data.RBMap.Basic
7-
import Mathlib.Init.Data.Nat.Notation
7+
import Mathlib.Data.Nat.Notation
88
import Mathlib.Mathport.Rename
99
import Mathlib.Tactic.TypeStar
1010
import Mathlib.Util.CompileInductive

‎Mathlib/Init/Data/Fin/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Leonardo de Moura
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77

88
/-!
99
# Note about `Mathlib/Init/`

‎Mathlib/Init/Data/Int/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad
66
The integers, with addition, multiplication, and subtraction.
77
-/
88
import Mathlib.Mathport.Rename
9-
import Mathlib.Init.Data.Nat.Notation
9+
import Mathlib.Data.Nat.Notation
1010

1111
/-!
1212
# Note about `Mathlib/Init/`

‎Mathlib/Init/Data/List/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Leonardo de Moura
55
-/
66
import Mathlib.Mathport.Rename
7-
import Mathlib.Init.Data.Nat.Notation
7+
import Mathlib.Data.Nat.Notation
88
import Batteries.Data.List.Basic
99

1010
/-!

‎Mathlib/Init/Data/Nat/Basic.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Floris van Doorn, Leonardo de Moura
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Mathport.Rename
88
import Mathlib.Util.CompileInductive
99

‎Mathlib/Init/Data/Nat/GCD.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
66
-/
77

88
import Batteries.Data.Nat.Gcd
9-
import Mathlib.Init.Data.Nat.Notation
9+
import Mathlib.Data.Nat.Notation
1010
import Mathlib.Mathport.Rename
1111

1212
#align_import init.data.nat.gcd from "leanprover-community/lean"@"855e5b74e3a52a40552e8f067169d747d48743fd"

‎Mathlib/Init/Data/Nat/Notation.lean

-22
This file was deleted.

‎Mathlib/Tactic/Linter/TextBased.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Michael Rothgang
55
-/
66

77
import Batteries.Data.String.Matcher
8-
import Mathlib.Init.Data.Nat.Notation
8+
import Mathlib.Data.Nat.Notation
99

1010
/-!
1111
## Text-based linters

‎Mathlib/Tactic/TFAE.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Johan Commelin, Reid Barton, Simon Hudon, Thomas Murrills, Mario Carneiro
55
-/
66
import Qq
7-
import Mathlib.Init.Data.Nat.Notation
7+
import Mathlib.Data.Nat.Notation
88
import Mathlib.Util.AtomM
99
import Mathlib.Data.List.TFAE
1010

‎Mathlib/Tactic/ToAdditive.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Mario Carneiro, Yury Kudryashov, Floris van Doorn, Jon Eugster
55
-/
6-
import Mathlib.Init.Data.Nat.Notation
6+
import Mathlib.Data.Nat.Notation
77
import Mathlib.Data.String.Defs
88
import Mathlib.Data.Array.Defs
99
import Mathlib.Lean.Expr.ReplaceRec

‎scripts/noshake.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@
4848
"Mathlib.Geometry.Manifold.Instances.Real",
4949
"Mathlib.Init.Align",
5050
"Mathlib.Init.Data.Int.Basic",
51-
"Mathlib.Init.Data.Nat.Notation",
51+
"Mathlib.Data.Nat.Notation",
5252
"Mathlib.LinearAlgebra.AffineSpace.Basic",
5353
"Mathlib.Mathport.Attributes",
5454
"Mathlib.Mathport.Notation",

‎test/Expr.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import Mathlib.Lean.Expr.ReplaceRec
2-
import Mathlib.Init.Data.Nat.Notation
2+
import Mathlib.Data.Nat.Notation
33
import Lean.Elab.Command
44

55
open Lean Meta Elab Command

‎test/apply_fun.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
import Mathlib.Init.Data.Nat.Notation
1+
import Mathlib.Data.Nat.Notation
22
import Mathlib.Tactic.Basic
33
import Mathlib.Tactic.ApplyFun
44
import Mathlib.Init.Function

‎test/cases.lean

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
import Mathlib.Tactic.Cases
22
import Mathlib.Init.Logic
3-
import Mathlib.Init.Data.Nat.Notation
3+
import Mathlib.Data.Nat.Notation
44

55
set_option autoImplicit true
66
example (x : α × β × γ) : True := by

0 commit comments

Comments
 (0)