From 11cb2b44d395eef07ac612b51fa19a0c9cd07a14 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Thu, 8 Sep 2022 10:32:14 +0000 Subject: [PATCH] fix(*): fix padding around notations (#16333) I noticed a bunch of issues around padding in mathport, so I went through and fixed all the padding issues I could find in mathlib. Co-authored-by: Yury G. Kudryashov --- archive/examples/prop_encodable.lean | 2 +- archive/sensitivity.lean | 4 ++-- src/algebra/big_operators/intervals.lean | 2 +- .../presheafed_space/gluing.lean | 8 ++++---- .../projective_spectrum/scheme.lean | 10 +++++----- src/algebraic_topology/simplicial_object.lean | 4 ++-- src/analysis/inner_product_space/l2_space.lean | 2 +- src/data/bracket.lean | 2 +- src/data/bundle.lean | 2 +- src/data/finset/fold.lean | 2 +- src/data/list/basic.lean | 4 ++-- src/data/list/perm.lean | 4 ++-- src/data/multiset/fold.lean | 2 +- src/data/nat/factorization/basic.lean | 4 ++-- src/data/rat/nnrat.lean | 2 +- src/data/rbtree/insert.lean | 2 +- src/data/real/nnreal.lean | 2 +- src/geometry/manifold/derivation_bundle.lean | 2 +- src/geometry/manifold/diffeomorph.lean | 4 ++-- src/group_theory/eckmann_hilton.lean | 2 +- src/linear_algebra/matrix/determinant.lean | 2 +- src/linear_algebra/span.lean | 2 +- src/linear_algebra/special_linear_group.lean | 2 +- src/linear_algebra/tensor_power.lean | 2 +- src/logic/function/basic.lean | 2 +- src/logic/relator.lean | 2 +- .../integral/divergence_theorem.lean | 8 ++++---- src/measure_theory/integral/torus_integral.lean | 16 ++++++++-------- src/order/basic.lean | 4 ++-- src/ring_theory/derivation.lean | 2 +- src/ring_theory/witt_vector/isocrystal.lean | 14 +++++++------- src/ring_theory/witt_vector/witt_polynomial.lean | 2 +- src/set_theory/cardinal/basic.lean | 2 +- src/set_theory/zfc/basic.lean | 2 +- src/tactic/omega/find_ees.lean | 10 +++++----- src/tactic/omega/int/preterm.lean | 6 +++--- src/tactic/omega/misc.lean | 2 +- src/tactic/omega/nat/preterm.lean | 2 +- src/tactic/reserved_notation.lean | 2 +- src/tactic/rewrite.lean | 2 +- .../uniform_space/abstract_completion.lean | 2 +- src/topology/uniform_space/basic.lean | 2 +- .../uniform_convergence_topology.lean | 6 +++--- test/noncomm_ring.lean | 2 +- test/simps.lean | 2 +- 45 files changed, 83 insertions(+), 83 deletions(-) diff --git a/archive/examples/prop_encodable.lean b/archive/examples/prop_encodable.lean index 64da2837b4f0b..4890ca2837d89 100644 --- a/archive/examples/prop_encodable.lean +++ b/archive/examples/prop_encodable.lean @@ -61,7 +61,7 @@ namespace prop_form private def constructors (α : Type*) := α ⊕ unit ⊕ unit ⊕ unit -local notation `cvar` a := sum.inl a +local notation `cvar ` a := sum.inl a local notation `cnot` := sum.inr (sum.inl unit.star) local notation `cand` := sum.inr (sum.inr (sum.inr unit.star)) local notation `cor` := sum.inr (sum.inr (sum.inl unit.star)) diff --git a/archive/sensitivity.lean b/archive/sensitivity.lean index 9c0342613cc0e..f1960b94e62ee 100644 --- a/archive/sensitivity.lean +++ b/archive/sensitivity.lean @@ -332,7 +332,7 @@ In this section, in order to enforce that `n` is positive, we write it as `m + 1` for some natural number `m`. -/ /-! `dim X` will denote the dimension of a subspace `X` as a cardinal. -/ -notation `dim` X:70 := module.rank ℝ ↥X +notation `dim ` X:70 := module.rank ℝ ↥X /-! `fdim X` will denote the (finite) dimension of a subspace `X` as a natural number. -/ notation `fdim` := finrank ℝ @@ -341,7 +341,7 @@ notation `Span` := submodule.span ℝ /-! `Card X` will denote the cardinal of a subset of a finite type, as a natural number. -/ -notation `Card` X:70 := X.to_finset.card +notation `Card ` X:70 := X.to_finset.card /-! In the following, `⊓` and `⊔` will denote intersection and sums of ℝ-subspaces, equipped with their subspace structures. The notations come from the general diff --git a/src/algebra/big_operators/intervals.lean b/src/algebra/big_operators/intervals.lean index 8a500766ee19a..baf2ae60a8faf 100644 --- a/src/algebra/big_operators/intervals.lean +++ b/src/algebra/big_operators/intervals.lean @@ -234,7 +234,7 @@ section module variables {R M : Type*} [ring R] [add_comm_group M] [module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ} open finset -- The partial sum of `g`, starting from zero -local notation `G` n:80 := ∑ i in range n, g i +local notation `G ` n:80 := ∑ i in range n, g i /-- **Summation by parts**, also known as **Abel's lemma** or an **Abel transformation** -/ theorem sum_Ico_by_parts (hmn : m < n) : diff --git a/src/algebraic_geometry/presheafed_space/gluing.lean b/src/algebraic_geometry/presheafed_space/gluing.lean index 94ef63d65c728..144ed3c721d9e 100644 --- a/src/algebraic_geometry/presheafed_space/gluing.lean +++ b/src/algebraic_geometry/presheafed_space/gluing.lean @@ -98,11 +98,11 @@ namespace glue_data variables {C} (D : glue_data C) local notation `𝖣` := D.to_glue_data -local notation `π₁` i `,` j `,` k := @pullback.fst _ _ _ _ _ (D.f i j) (D.f i k) _ -local notation `π₂` i `,` j `,` k := @pullback.snd _ _ _ _ _ (D.f i j) (D.f i k) _ -local notation `π₁⁻¹` i `,` j `,` k := +local notation `π₁ `i`, `j`, `k := @pullback.fst _ _ _ _ _ (D.f i j) (D.f i k) _ +local notation `π₂ `i`, `j`, `k := @pullback.snd _ _ _ _ _ (D.f i j) (D.f i k) _ +local notation `π₁⁻¹ `i`, `j`, `k := (PresheafedSpace.is_open_immersion.pullback_fst_of_right (D.f i j) (D.f i k)).inv_app -local notation `π₂⁻¹` i `,` j `,` k := +local notation `π₂⁻¹ `i`, `j`, `k := (PresheafedSpace.is_open_immersion.pullback_snd_of_left (D.f i j) (D.f i k)).inv_app /-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces. -/ diff --git a/src/algebraic_geometry/projective_spectrum/scheme.lean b/src/algebraic_geometry/projective_spectrum/scheme.lean index d99ce60d766e8..06965cb6ab393 100644 --- a/src/algebraic_geometry/projective_spectrum/scheme.lean +++ b/src/algebraic_geometry/projective_spectrum/scheme.lean @@ -79,13 +79,13 @@ local notation `Proj| ` U := Proj .restrict (opens.open_embedding (U : opens Pro local notation `Proj.T| ` U := (Proj .restrict (opens.open_embedding (U : opens Proj.T))).to_SheafedSpace.to_PresheafedSpace.1 -- the underlying topological space of `Proj` restricted to some open set -local notation `pbo` x := projective_spectrum.basic_open 𝒜 x +local notation `pbo ` x := projective_spectrum.basic_open 𝒜 x -- basic open sets in `Proj` -local notation `sbo` f := prime_spectrum.basic_open f +local notation `sbo ` f := prime_spectrum.basic_open f -- basic open sets in `Spec` -local notation `Spec` ring := Spec.LocallyRingedSpace_obj (CommRing.of ring) +local notation `Spec ` ring := Spec.LocallyRingedSpace_obj (CommRing.of ring) -- `Spec` as a locally ringed space -local notation `Spec.T` ring := +local notation `Spec.T ` ring := (Spec.LocallyRingedSpace_obj (CommRing.of ring)).to_SheafedSpace.to_PresheafedSpace.1 -- the underlying topological space of `Spec` @@ -121,7 +121,7 @@ def degree_zero_part {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) : subring (away f) end -local notation `A⁰_` f_deg := degree_zero_part f_deg +local notation `A⁰_ ` f_deg := degree_zero_part f_deg section diff --git a/src/algebraic_topology/simplicial_object.lean b/src/algebraic_topology/simplicial_object.lean index 3bbdcf4a7e6ad..b6fc69fe884cc 100644 --- a/src/algebraic_topology/simplicial_object.lean +++ b/src/algebraic_topology/simplicial_object.lean @@ -36,7 +36,7 @@ def simplicial_object := simplex_categoryᵒᵖ ⥤ C namespace simplicial_object -localized "notation (name := simplicial_object.at) X `_[`:1000 n `]` := +localized "notation (name := simplicial_object.at) X ` _[`:1000 n `]` := (X : category_theory.simplicial_object hole!).obj (opposite.op (simplex_category.mk n))" in simplicial @@ -265,7 +265,7 @@ def cosimplicial_object := simplex_category ⥤ C namespace cosimplicial_object -localized "notation (name := cosimplicial_object.at) X `_[`:1000 n `]` := +localized "notation (name := cosimplicial_object.at) X ` _[`:1000 n `]` := (X : category_theory.cosimplicial_object hole!).obj (simplex_category.mk n)" in simplicial instance {J : Type v} [small_category J] [has_limits_of_shape J C] : diff --git a/src/analysis/inner_product_space/l2_space.lean b/src/analysis/inner_product_space/l2_space.lean index 5257cbb58485f..4d7510f4504f2 100644 --- a/src/analysis/inner_product_space/l2_space.lean +++ b/src/analysis/inner_product_space/l2_space.lean @@ -89,7 +89,7 @@ variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [inner_product_space 𝕜 variables {G : ι → Type*} [Π i, inner_product_space 𝕜 (G i)] local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y -notation `ℓ²(` ι `,` 𝕜 `)` := lp (λ i : ι, 𝕜) 2 +notation `ℓ²(`ι`, `𝕜`)` := lp (λ i : ι, 𝕜) 2 /-! ### Inner product space structure on `lp G 2` -/ diff --git a/src/data/bracket.lean b/src/data/bracket.lean index e5cb5e55f2ff4..4372992dcfd76 100644 --- a/src/data/bracket.lean +++ b/src/data/bracket.lean @@ -34,4 +34,4 @@ these are the Unicode "square with quill" brackets rather than the usual square `K` of a group. -/ class has_bracket (L M : Type*) := (bracket : L → M → M) -notation `⁅`x`,` y`⁆` := has_bracket.bracket x y +notation `⁅`x`, `y`⁆` := has_bracket.bracket x y diff --git a/src/data/bundle.lean b/src/data/bundle.lean index 946d03f62ac00..30eb9875bdb20 100644 --- a/src/data/bundle.lean +++ b/src/data/bundle.lean @@ -73,7 +73,7 @@ instance {x : B} : has_coe_t (E x) (total_space E) := ⟨total_space_mk x⟩ lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = total_space_mk x v := rfl -- notation for the direct sum of two bundles over the same base -notation E₁ `×ᵇ`:100 E₂ := λ x, E₁ x × E₂ x +notation E₁ ` ×ᵇ `:100 E₂ := λ x, E₁ x × E₂ x /-- `bundle.trivial B F` is the trivial bundle over `B` of fiber `F`. -/ def trivial (B : Type*) (F : Type*) : B → Type* := function.const B F diff --git a/src/data/finset/fold.lean b/src/data/finset/fold.lean index a6db4aa26f38e..31120d6e4bc95 100644 --- a/src/data/finset/fold.lean +++ b/src/data/finset/fold.lean @@ -18,7 +18,7 @@ variables {α β γ : Type*} /-! ### fold -/ section fold variables (op : β → β → β) [hc : is_commutative β op] [ha : is_associative β op] -local notation (name := op) a * b := op a b +local notation (name := op) a ` * ` b := op a b include hc ha /-- `fold op b f s` folds the commutative associative operation `op` over the diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index eadbb338f32c9..1dca88a4290fc 100644 --- a/src/data/list/basic.lean +++ b/src/data/list/basic.lean @@ -2459,8 +2459,8 @@ end foldl_eq_foldlr' section variables {op : α → α → α} [ha : is_associative α op] [hc : is_commutative α op] -local notation (name := op) a * b := op a b -local notation (name := foldl) l <*> a := foldl op a l +local notation (name := op) a ` * ` b := op a b +local notation (name := foldl) l ` <*> ` a := foldl op a l include ha diff --git a/src/data/list/perm.lean b/src/data/list/perm.lean index cacfad8a95820..73c8662d851c8 100644 --- a/src/data/list/perm.lean +++ b/src/data/list/perm.lean @@ -457,8 +457,8 @@ end section variables {op : α → α → α} [is_associative α op] [is_commutative α op] -local notation (name := op) a * b := op a b -local notation (name := foldl) l <*> a := foldl op a l +local notation (name := op) a ` * ` b := op a b +local notation (name := foldl) l ` <*> ` a := foldl op a l lemma perm.fold_op_eq {l₁ l₂ : list α} {a : α} (h : l₁ ~ l₂) : l₁ <*> a = l₂ <*> a := h.foldl_eq (right_comm _ is_commutative.comm is_associative.assoc) _ diff --git a/src/data/multiset/fold.lean b/src/data/multiset/fold.lean index ff8c7fc44d233..94e79d0543047 100644 --- a/src/data/multiset/fold.lean +++ b/src/data/multiset/fold.lean @@ -16,7 +16,7 @@ variables {α β : Type*} /-! ### fold -/ section fold variables (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op] -local notation (name := op) a * b := op a b +local notation (name := op) a ` * ` b := op a b include hc ha /-- `fold op b s` folds a commutative associative operation `op` over diff --git a/src/data/nat/factorization/basic.lean b/src/data/nat/factorization/basic.lean index 5510beae7791e..ca5f59e2c4e80 100644 --- a/src/data/nat/factorization/basic.lean +++ b/src/data/nat/factorization/basic.lean @@ -291,8 +291,8 @@ the $p$-adic order/valuation of a number, and `proj` and `compl` are for the pro complementary projection. The term `n.factorization p` is the $p$-adic order itself. For example, `ord_proj[2] n` is the even part of `n` and `ord_compl[2] n` is the odd part. -/ -notation `ord_proj[` p `]` n:max := p ^ (nat.factorization n p) -notation `ord_compl[` p `]` n:max := n / ord_proj[p] n +notation `ord_proj[` p `] ` n:max := p ^ (nat.factorization n p) +notation `ord_compl[` p `] ` n:max := n / ord_proj[p] n @[simp] lemma ord_proj_of_not_prime (n p : ℕ) (hp : ¬ p.prime) : ord_proj[p] n = 1 := by simp [factorization_eq_zero_of_non_prime n hp] diff --git a/src/data/rat/nnrat.lean b/src/data/rat/nnrat.lean index 8b14701c39ca4..29e05d2d872e2 100644 --- a/src/data/rat/nnrat.lean +++ b/src/data/rat/nnrat.lean @@ -31,7 +31,7 @@ open_locale big_operators densely_ordered, archimedean, inhabited]] def nnrat := {q : ℚ // 0 ≤ q} -localized "notation ` ℚ≥0 ` := nnrat" in nnrat +localized "notation (name := nnrat) `ℚ≥0` := nnrat" in nnrat namespace nnrat variables {α : Type*} {p q : ℚ≥0} diff --git a/src/data/rbtree/insert.lean b/src/data/rbtree/insert.lean index 22bbd2934e4a9..955270781fd37 100644 --- a/src/data/rbtree/insert.lean +++ b/src/data/rbtree/insert.lean @@ -188,7 +188,7 @@ parameters {α : Type u} (lt : α → α → Prop) local attribute [simp] mem balance1_node balance2_node -local infix (name := mem) `∈` := mem lt +local infix (name := mem) ` ∈ ` := mem lt lemma mem_balance1_node_of_mem_left {x s} (v) (t : rbnode α) : x ∈ s → x ∈ balance1_node s v t := begin diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean index 12a5b2942c8f6..7af447cae0bee 100644 --- a/src/data/real/nnreal.lean +++ b/src/data/real/nnreal.lean @@ -59,7 +59,7 @@ open_locale classical big_operators linear_ordered_semiring, ordered_comm_semiring, canonically_ordered_comm_semiring, has_sub, has_ordered_sub, has_div, inhabited]] def nnreal := {r : ℝ // 0 ≤ r} -localized "notation (name := nnreal) ` ℝ≥0 ` := nnreal" in nnreal +localized "notation (name := nnreal) `ℝ≥0` := nnreal" in nnreal namespace nnreal diff --git a/src/geometry/manifold/derivation_bundle.lean b/src/geometry/manifold/derivation_bundle.lean index 0bc52955e9860..f463781aa276b 100644 --- a/src/geometry/manifold/derivation_bundle.lean +++ b/src/geometry/manifold/derivation_bundle.lean @@ -35,7 +35,7 @@ instance smooth_functions_tower : is_scalar_tower 𝕜 C^∞⟮I, M; 𝕜⟯ C^ which is defined as `f • r = f(x) * r`. -/ @[nolint unused_arguments] def pointed_smooth_map (x : M) := C^n⟮I, M; 𝕜⟯ -localized "notation (name := pointed_smooth_map) `C^` n `⟮` I `,` M `;` 𝕜 `⟯⟨` x `⟩` := +localized "notation (name := pointed_smooth_map) `C^` n `⟮` I `, ` M `; ` 𝕜 `⟯⟨` x `⟩` := pointed_smooth_map 𝕜 I M n x" in derivation variables {𝕜 M} diff --git a/src/geometry/manifold/diffeomorph.lean b/src/geometry/manifold/diffeomorph.lean index a9968eaaf5ffc..cead8e7582a07 100644 --- a/src/geometry/manifold/diffeomorph.lean +++ b/src/geometry/manifold/diffeomorph.lean @@ -77,9 +77,9 @@ structure diffeomorph extends M ≃ M' := end defs -localized "notation (name := diffeomorph) M ` ≃ₘ^` n:1000 `⟮`:50 I `,` J `⟯ ` N := +localized "notation (name := diffeomorph) M ` ≃ₘ^` n:1000 `⟮`:50 I `, ` J `⟯ ` N := diffeomorph I J M N n" in manifold -localized "notation (name := diffeomorph.top) M ` ≃ₘ⟮` I `,` J `⟯ ` N := +localized "notation (name := diffeomorph.top) M ` ≃ₘ⟮` I `, ` J `⟯ ` N := diffeomorph I J M N ⊤" in manifold localized "notation (name := diffeomorph.self) E ` ≃ₘ^` n:1000 `[`:50 𝕜 `] ` E' := diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n" in manifold diff --git a/src/group_theory/eckmann_hilton.lean b/src/group_theory/eckmann_hilton.lean index 9ac8e44c83bdc..3cbc0aadc8db5 100644 --- a/src/group_theory/eckmann_hilton.lean +++ b/src/group_theory/eckmann_hilton.lean @@ -27,7 +27,7 @@ universe u namespace eckmann_hilton variables {X : Type u} -local notation a `<`m`>` b := m a b +local notation a ` <`m`> ` b := m a b /-- `is_unital m e` expresses that `e : X` is a left and right unit for the binary operation `m : X → X → X`. -/ diff --git a/src/linear_algebra/matrix/determinant.lean b/src/linear_algebra/matrix/determinant.lean index fd0e426dc7da5..8c398e048380f 100644 --- a/src/linear_algebra/matrix/determinant.lean +++ b/src/linear_algebra/matrix/determinant.lean @@ -47,7 +47,7 @@ open_locale matrix big_operators variables {m n : Type*} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m] variables {R : Type v} [comm_ring R] -local notation `ε` σ:max := ((sign σ : ℤ ) : R) +local notation `ε ` σ:max := ((sign σ : ℤ) : R) /-- `det` is an `alternating_map` in the rows of the matrix. -/ diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean index 068fdef67622b..0ead5fe1ea603 100644 --- a/src/linear_algebra/span.lean +++ b/src/linear_algebra/span.lean @@ -202,7 +202,7 @@ by rw [submodule.span_union, p.span_eq] /- Note that the character `∙` U+2219 used below is different from the scalar multiplication character `•` U+2022 and the matrix multiplication character `⬝` U+2B1D. -/ -notation R`∙`:1000 x := span R (@singleton _ _ set.has_singleton x) +notation R` ∙ `:1000 x := span R (@singleton _ _ set.has_singleton x) lemma span_eq_supr_of_singleton_spans (s : set M) : span R s = ⨆ x ∈ s, R ∙ x := by simp only [←span_Union, set.bUnion_of_singleton s] diff --git a/src/linear_algebra/special_linear_group.lean b/src/linear_algebra/special_linear_group.lean index f7293f4a62192..d371eab1cda05 100644 --- a/src/linear_algebra/special_linear_group.lean +++ b/src/linear_algebra/special_linear_group.lean @@ -63,7 +63,7 @@ def special_linear_group := { A : matrix n n R // A.det = 1 } end localized "notation (name := special_linear_group.fin) - `SL(` n `,` R `)`:= matrix.special_linear_group (fin n) R" in matrix_groups + `SL(`n`, `R`)`:= matrix.special_linear_group (fin n) R" in matrix_groups namespace special_linear_group diff --git a/src/linear_algebra/tensor_power.lean b/src/linear_algebra/tensor_power.lean index 360f289e3870e..abb55292695bc 100644 --- a/src/linear_algebra/tensor_power.lean +++ b/src/linear_algebra/tensor_power.lean @@ -66,7 +66,7 @@ def mul_equiv {n m : ℕ} : (⨂[R]^n M) ⊗[R] (⨂[R]^m M) ≃ₗ[R] ⨂[R]^(n instance ghas_mul : graded_monoid.ghas_mul (λ i, ⨂[R]^i M) := { mul := λ i j a b, mul_equiv (a ⊗ₜ b) } -local infix `ₜ*`:70 := @graded_monoid.ghas_mul.mul ℕ (λ i, ⨂[R]^i M) _ _ _ _ +local infix ` ₜ* `:70 := @graded_monoid.ghas_mul.mul ℕ (λ i, ⨂[R]^i M) _ _ _ _ lemma ghas_mul_def {i j} (a : ⨂[R]^i M) (b : ⨂[R]^j M) : a ₜ* b = mul_equiv (a ⊗ₜ b) := rfl diff --git a/src/logic/function/basic.lean b/src/logic/function/basic.lean index 4a8e328352e8e..427d6f658d8db 100644 --- a/src/logic/function/basic.lean +++ b/src/logic/function/basic.lean @@ -622,7 +622,7 @@ def bicompr (f : γ → δ) (g : α → β → γ) (a b) := f (g a b) -- Suggested local notation: -local notation f `∘₂` g := bicompr f g +local notation f ` ∘₂ ` g := bicompr f g lemma uncurry_bicompr (f : α → β → γ) (g : γ → δ) : uncurry (g ∘₂ f) = (g ∘ uncurry f) := rfl diff --git a/src/logic/relator.lean b/src/logic/relator.lean index 30aa8a5230e81..c9ea9b0afedac 100644 --- a/src/logic/relator.lean +++ b/src/logic/relator.lean @@ -26,7 +26,7 @@ variables (R : α → β → Prop) (S : γ → δ → Prop) def lift_fun (f : α → γ) (g : β → δ) : Prop := ∀⦃a b⦄, R a b → S (f a) (g b) -infixr ⇒ := lift_fun +infixr ` ⇒ ` := lift_fun end diff --git a/src/measure_theory/integral/divergence_theorem.lean b/src/measure_theory/integral/divergence_theorem.lean index 35585f5fc6dcb..8210300518012 100644 --- a/src/measure_theory/integral/divergence_theorem.lean +++ b/src/measure_theory/integral/divergence_theorem.lean @@ -61,7 +61,7 @@ variables {n : ℕ} local notation `ℝⁿ` := fin n → ℝ local notation `ℝⁿ⁺¹` := fin (n + 1) → ℝ local notation `Eⁿ⁺¹` := fin (n + 1) → E -local notation `e` i := pi.single i 1 +local notation `e ` i := pi.single i 1 section @@ -230,9 +230,9 @@ end variables (a b : ℝⁿ⁺¹) -local notation `face` i := set.Icc (a ∘ fin.succ_above i) (b ∘ fin.succ_above i) -local notation `front_face` i:2000 := fin.insert_nth i (b i) -local notation `back_face` i:2000 := fin.insert_nth i (a i) +local notation `face ` i := set.Icc (a ∘ fin.succ_above i) (b ∘ fin.succ_above i) +local notation `front_face ` i:2000 := fin.insert_nth i (b i) +local notation `back_face ` i:2000 := fin.insert_nth i (a i) /-- **Divergence theorem** for Bochner integral. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is continuous on a rectangular box `[a, b] : set ℝⁿ⁺¹`, `a ≤ b`, is differentiable on its interior with derivative diff --git a/src/measure_theory/integral/torus_integral.lean b/src/measure_theory/integral/torus_integral.lean index 01fdf2694ed15..d13836f451806 100644 --- a/src/measure_theory/integral/torus_integral.lean +++ b/src/measure_theory/integral/torus_integral.lean @@ -60,14 +60,14 @@ noncomputable theory open complex set measure_theory function filter topological_space open_locale real big_operators -local notation `ℝ⁰`:= fin 0 → ℝ -local notation `ℂ⁰`:= fin 0 → ℂ -local notation `ℝ¹`:= fin 1 → ℝ -local notation `ℂ¹`:= fin 1 → ℂ -local notation `ℝⁿ`:= fin n → ℝ -local notation `ℂⁿ`:= fin n → ℂ -local notation `ℝⁿ⁺¹`:= fin (n + 1) → ℝ -local notation `ℂⁿ⁺¹`:= fin (n + 1) → ℂ +local notation `ℝ⁰` := fin 0 → ℝ +local notation `ℂ⁰` := fin 0 → ℂ +local notation `ℝ¹` := fin 1 → ℝ +local notation `ℂ¹` := fin 1 → ℂ +local notation `ℝⁿ` := fin n → ℝ +local notation `ℂⁿ` := fin n → ℂ +local notation `ℝⁿ⁺¹` := fin (n + 1) → ℝ +local notation `ℂⁿ⁺¹` := fin (n + 1) → ℂ /-! ### `torus_map`, a generalization of a torus diff --git a/src/order/basic.lean b/src/order/basic.lean index 1e4188049bb58..cb0ffdeaba3da 100644 --- a/src/order/basic.lean +++ b/src/order/basic.lean @@ -555,8 +555,8 @@ end min_max_rec /-- Typeclass for the `⊓` (`\glb`) notation -/ @[notation_class] class has_inf (α : Type u) := (inf : α → α → α) -infix ⊔ := has_sup.sup -infix ⊓ := has_inf.inf +infix ` ⊔ ` := has_sup.sup +infix ` ⊓ ` := has_inf.inf /-! ### Lifts of order instances -/ diff --git a/src/ring_theory/derivation.lean b/src/ring_theory/derivation.lean index 3f249a07dd6f6..903b95af667f5 100644 --- a/src/ring_theory/derivation.lean +++ b/src/ring_theory/derivation.lean @@ -563,7 +563,7 @@ Note that the slash is `\textfractionsolidus`. @[derive [add_comm_group, module R, module S, module (S ⊗[R] S)]] def kaehler_differential : Type* := (kaehler_differential.ideal R S).cotangent -notation `Ω[ `:100 S ` ⁄ `:0 R ` ]`:0 := kaehler_differential R S +notation `Ω[`:100 S `⁄`:0 R `]`:0 := kaehler_differential R S instance : nonempty Ω[S⁄R] := ⟨0⟩ diff --git a/src/ring_theory/witt_vector/isocrystal.lean b/src/ring_theory/witt_vector/isocrystal.lean index 853f192542547..74f49caeefa05 100644 --- a/src/ring_theory/witt_vector/isocrystal.lean +++ b/src/ring_theory/witt_vector/isocrystal.lean @@ -59,7 +59,7 @@ namespace witt_vector variables (p : ℕ) [fact p.prime] variables (k : Type*) [comm_ring k] localized "notation (name := witt_vector.fraction_ring) - `K(` p`,` k`)` := fraction_ring (witt_vector p k)" in isocrystal + `K(`p`, `k`)` := fraction_ring (witt_vector p k)" in isocrystal section perfect_ring variables [is_domain k] [char_p k p] [perfect_ring k p] @@ -74,7 +74,7 @@ is_fraction_ring.field_equiv_of_ring_equiv (frobenius_equiv p k) def fraction_ring.frobenius_ring_hom : K(p, k) →+* K(p, k) := fraction_ring.frobenius p k localized "notation (name := witt_vector.frobenius_ring_hom) - `φ(` p`,` k`)` := witt_vector.fraction_ring.frobenius_ring_hom p k" in isocrystal + `φ(`p`, `k`)` := witt_vector.fraction_ring.frobenius_ring_hom p k" in isocrystal instance inv_pair₁ : ring_hom_inv_pair (φ(p, k)) _ := ring_hom_inv_pair.of_ring_equiv (fraction_ring.frobenius p k) @@ -83,9 +83,9 @@ instance inv_pair₂ : ring_hom_inv_pair ((fraction_ring.frobenius p k).symm : K(p, k) →+* K(p, k)) _ := ring_hom_inv_pair.of_ring_equiv (fraction_ring.frobenius p k).symm -localized "notation (name := frobenius_ring_hom.linear_map) M ` →ᶠˡ[`:50 p `,` k `] ` M₂ := +localized "notation (name := frobenius_ring_hom.linear_map) M ` →ᶠˡ[`:50 p `, ` k `] ` M₂ := linear_map (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂" in isocrystal -localized "notation (name := frobenius_ring_hom.linear_equiv) M ` ≃ᶠˡ[`:50 p `,` k `] ` M₂ := +localized "notation (name := frobenius_ring_hom.linear_equiv) M ` ≃ᶠˡ[`:50 p `, ` k `] ` M₂ := linear_equiv (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂" in isocrystal /-! ### Isocrystals -/ @@ -108,7 +108,7 @@ Project the Frobenius automorphism from an isocrystal. Denoted by `Φ(p, k)` whe def isocrystal.frobenius : V ≃ᶠˡ[p, k] V := @isocrystal.frob p _ k _ _ _ _ _ _ _ variables (V) -localized "notation `Φ(` p`,` k`)` := witt_vector.isocrystal.frobenius p k" in isocrystal +localized "notation `Φ(`p`, `k`)` := witt_vector.isocrystal.frobenius p k" in isocrystal /-- A homomorphism between isocrystals respects the Frobenius map. -/ @[nolint has_nonempty_instance] @@ -121,9 +121,9 @@ structure isocrystal_equiv extends V ≃ₗ[K(p, k)] V₂ := ( frob_equivariant : ∀ x : V, Φ(p, k) (to_linear_equiv x) = to_linear_equiv (Φ(p, k) x) ) localized "notation (name := isocrystal_hom) - M ` →ᶠⁱ[`:50 p `,` k `] ` M₂ := witt_vector.isocrystal_hom p k M M₂" in isocrystal + M ` →ᶠⁱ[`:50 p `, ` k `] ` M₂ := witt_vector.isocrystal_hom p k M M₂" in isocrystal localized "notation (name := isocrystal_equiv) - M ` ≃ᶠⁱ[`:50 p `,` k `] ` M₂ := witt_vector.isocrystal_equiv p k M M₂" in isocrystal + M ` ≃ᶠⁱ[`:50 p `, ` k `] ` M₂ := witt_vector.isocrystal_equiv p k M M₂" in isocrystal end perfect_ring diff --git a/src/ring_theory/witt_vector/witt_polynomial.lean b/src/ring_theory/witt_vector/witt_polynomial.lean index 8a4a5d7e6fc46..5d20e8308e910 100644 --- a/src/ring_theory/witt_vector/witt_polynomial.lean +++ b/src/ring_theory/witt_vector/witt_polynomial.lean @@ -90,7 +90,7 @@ This allows us to simply write `W n` or `W_ ℤ n`. -/ -- Notation with ring of coefficients explicit localized "notation (name := witt_polynomial) `W_` := witt_polynomial p" in witt -- Notation with ring of coefficients implicit -localized "notation (name := witt_polynomial.infer) `W` := witt_polynomial p hole!" in witt +localized "notation (name := witt_polynomial.infer) `W` := witt_polynomial p hole!" in witt open_locale witt open mv_polynomial diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index 2798b655518f7..e94aa2580d581 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -103,7 +103,7 @@ namespace cardinal /-- The cardinal number of a type -/ def mk : Type u → cardinal := quotient.mk -localized "notation (name := cardinal.mk) `#` := cardinal.mk" in cardinal +localized "prefix (name := cardinal.mk) `#` := cardinal.mk" in cardinal instance can_lift_cardinal_Type : can_lift cardinal.{u} (Type u) := ⟨mk, λ c, true, λ c _, quot.induction_on c $ λ α, ⟨α, rfl⟩⟩ diff --git a/src/set_theory/zfc/basic.lean b/src/set_theory/zfc/basic.lean index 3447accd70398..df5bbe6c3c911 100644 --- a/src/set_theory/zfc/basic.lean +++ b/src/set_theory/zfc/basic.lean @@ -931,7 +931,7 @@ mem_univ.2 $ or.elim (classical.em $ ∃ x, ∀ y, A y ↔ y = x) /-- Function value -/ def fval (F A : Class.{u}) : Class.{u} := iota (λ y, to_Set (λ x, F (Set.pair x y)) A) -infixl `′`:100 := fval +infixl ` ′ `:100 := fval theorem fval_ex (F A : Class.{u}) : F ′ A ∈ univ.{u} := iota_ex _ diff --git a/src/tactic/omega/find_ees.lean b/src/tactic/omega/find_ees.lean index 9529649b46846..83968c777d898 100644 --- a/src/tactic/omega/find_ees.lean +++ b/src/tactic/omega/find_ees.lean @@ -79,7 +79,7 @@ do x ← ((t1 >>= return ∘ some) <|> return none), | (some a) := t3 a end -local notation t1 `!>>=` t2 `;` t3 := ee_commit t1 t2 t3 +local notation t1 ` !>>= ` t2 `; ` t3 := ee_commit t1 t2 t3 private meta def of_tactic {α : Type} : tactic α → eqelim α := state_t.lift @@ -126,8 +126,8 @@ do (i,n) ← find_min_coeff_core t.snd, meta def elim_eq : eqelim unit := do t ← head_eq, i ← get_gcd t, - factor i t !>>= (set_eqs [] >> add_ee (ee.nondiv i)) ; -λ s, find_min_coeff s !>>= add_ee ee.drop ; + factor i t !>>= (set_eqs [] >> add_ee (ee.nondiv i)); +λ s, find_min_coeff s !>>= add_ee ee.drop; λ ⟨i, n, u⟩, if i = 1 then do eqs ← get_eqs, @@ -147,11 +147,11 @@ else let v : term := coeffs_reduce n u.fst u.snd in /-- Find and return the sequence of steps for eliminating all equality constraints in the current state. -/ meta def elim_eqs : eqelim (list ee) := -elim_eq !>>= get_ees ; λ _, elim_eqs +elim_eq !>>= get_ees; λ _, elim_eqs /-- Given a linear constrain clause, return a list of steps for eliminating its equality constraints. -/ meta def find_ees : clause → tactic (list ee) -| (eqs,les) := run eqs les elim_eqs +| (eqs, les) := run eqs les elim_eqs end omega diff --git a/src/tactic/omega/int/preterm.lean b/src/tactic/omega/int/preterm.lean index dafc9fc939d60..5d793e5325c99 100644 --- a/src/tactic/omega/int/preterm.lean +++ b/src/tactic/omega/int/preterm.lean @@ -32,9 +32,9 @@ inductive preterm : Type | var : int → nat → preterm | add : preterm → preterm → preterm -localized "notation (name := preterm.cst) `&` k := omega.int.preterm.cst k" in omega.int -localized "infix (name := preterm.var) ` ** ` : 300 := omega.int.preterm.var" in omega.int -localized "notation (name := preterm.add) t `+*` s := omega.int.preterm.add t s" in omega.int +localized "notation (name := preterm.cst) `&` k := omega.int.preterm.cst k" in omega.int +localized "infix (name := preterm.var) ` ** `:300 := omega.int.preterm.var" in omega.int +localized "notation (name := preterm.add) t ` +* ` s := omega.int.preterm.add t s" in omega.int namespace preterm diff --git a/src/tactic/omega/misc.lean b/src/tactic/omega/misc.lean index adb61ec932185..2931b7282e1eb 100644 --- a/src/tactic/omega/misc.lean +++ b/src/tactic/omega/misc.lean @@ -31,7 +31,7 @@ lemma pred_mono_2' {c : Prop → Prop → Prop} {a1 a2 b1 b2 : Prop} : def update (m : nat) (a : α) (v : nat → α) : nat → α | n := if n = m then a else v n -localized "notation (name := omega.update) v ` ⟨` m ` ↦ ` a `⟩` := omega.update m a v" in omega +localized "notation (name := omega.update) v ` ⟨`m` ↦ `a`⟩` := omega.update m a v" in omega lemma update_eq (m : nat) (a : α) (v : nat → α) : (v ⟨m ↦ a⟩) m = a := by simp only [update, if_pos rfl] diff --git a/src/tactic/omega/nat/preterm.lean b/src/tactic/omega/nat/preterm.lean index a0ef3c187fda2..b55af2eb58577 100644 --- a/src/tactic/omega/nat/preterm.lean +++ b/src/tactic/omega/nat/preterm.lean @@ -37,7 +37,7 @@ inductive preterm : Type | sub : preterm → preterm → preterm localized "notation (name := preterm.cst) `&` k := omega.nat.preterm.cst k" in omega.nat -localized "infix (name := preterm.var) ` ** ` : 300 := omega.nat.preterm.var" in omega.nat +localized "infix (name := preterm.var) ` ** `:300 := omega.nat.preterm.var" in omega.nat localized "notation (name := preterm.add) t ` +* ` s := omega.nat.preterm.add t s" in omega.nat localized "notation (name := preterm.sub) t ` -* ` s := omega.nat.preterm.sub t s" in omega.nat diff --git a/src/tactic/reserved_notation.lean b/src/tactic/reserved_notation.lean index 0f18d64545518..d34358ece4121 100644 --- a/src/tactic/reserved_notation.lean +++ b/src/tactic/reserved_notation.lean @@ -60,4 +60,4 @@ reserve infixl ` ⊔ `:68 reserve infix ` ≃ₗ `:25 -- used in `data/matrix/notation.lean` -reserve notation `!![` +reserve notation `!![` diff --git a/src/tactic/rewrite.lean b/src/tactic/rewrite.lean index 6fee7e9216cb9..8398ceae981d8 100644 --- a/src/tactic/rewrite.lean +++ b/src/tactic/rewrite.lean @@ -204,7 +204,7 @@ It works for any function `f` for which an `is_associative f` instance can be fo ``` example {α : Type*} (f : α → α → α) [is_associative α f] (a b c d x : α) : - let infix `~` := f in + let infix ` ~ ` := f in b ~ c = x → (a ~ b ~ c ~ d) = (a ~ x ~ d) := begin intro h, diff --git a/src/topology/uniform_space/abstract_completion.lean b/src/topology/uniform_space/abstract_completion.lean index 6c5960557923b..75c54a385929b 100644 --- a/src/topology/uniform_space/abstract_completion.lean +++ b/src/topology/uniform_space/abstract_completion.lean @@ -299,7 +299,7 @@ variables {γ : Type*} [uniform_space γ] (pkg'' : abstract_completion γ) local notation `hatγ` := pkg''.space local notation `ι''` := pkg''.coe -local notation f `∘₂` g := bicompr f g +local notation f ` ∘₂ ` g := bicompr f g /-- Lift two variable maps to completions. -/ protected def map₂ (f : α → β → γ) : hatα → hatβ → hatγ := diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index c63b90d52d037..fe33e6b76513c 100644 --- a/src/topology/uniform_space/basic.lean +++ b/src/topology/uniform_space/basic.lean @@ -1473,7 +1473,7 @@ open uniform_space function variables {δ' : Type*} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] [uniform_space δ'] -local notation f `∘₂` g := function.bicompr f g +local notation f ` ∘₂ ` g := function.bicompr f g /-- Uniform continuity for functions of two variables. -/ def uniform_continuous₂ (f : α → β → γ) := uniform_continuous (uncurry f) diff --git a/src/topology/uniform_space/uniform_convergence_topology.lean b/src/topology/uniform_space/uniform_convergence_topology.lean index 5915f96223940..92fdd99b70693 100644 --- a/src/topology/uniform_space/uniform_convergence_topology.lean +++ b/src/topology/uniform_space/uniform_convergence_topology.lean @@ -222,7 +222,7 @@ protected def uniform_space : uniform_space (α → β) := uniform_space.of_core (uniform_convergence.uniform_core α β) local attribute [instance] uniform_convergence.uniform_space -local notation `𝒰(` α `,` β `,` u `)` := @uniform_convergence.uniform_space α β u +local notation `𝒰(`α`, `β`, `u`)` := @uniform_convergence.uniform_space α β u /-- By definition, the uniformity of `α → β` endowed with the structure of uniform convergence on `α` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a filter basis. -/ @@ -472,7 +472,7 @@ namespace uniform_convergence_on variables (α β : Type*) {γ ι : Type*} [uniform_space β] (𝔖 : set (set α)) variables {F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α} -local notation `𝒰(` α `,` β `,` u `)` := @uniform_convergence.uniform_space α β u +local notation `𝒰(`α`, `β`, `u`)` := @uniform_convergence.uniform_space α β u /-- Uniform structure of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`. It is defined as the infimum, for `S ∈ 𝔖`, of the pullback of `𝒰 S β` by `S.restrict`, the @@ -482,7 +482,7 @@ protected def uniform_space : uniform_space (α → β) := ⨅ (s : set α) (hs : s ∈ 𝔖), uniform_space.comap s.restrict (𝒰(s, β, _)) -local notation `𝒱(` α `,` β `,` 𝔖 `,` u `)` := @uniform_convergence_on.uniform_space α β u 𝔖 +local notation `𝒱(`α`, `β`, `𝔖`, `u`)` := @uniform_convergence_on.uniform_space α β u 𝔖 /-- Topology of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`. -/ protected def topological_space : topological_space (α → β) := diff --git a/test/noncomm_ring.lean b/test/noncomm_ring.lean index 47e487c84a3e4..8fcb1ce3d0545 100644 --- a/test/noncomm_ring.lean +++ b/test/noncomm_ring.lean @@ -1,6 +1,6 @@ import tactic.noncomm_ring -local notation (name := commutator) `⁅`a`,` b`⁆` := a * b - b * a +local notation (name := commutator) `⁅`a`, `b`⁆` := a * b - b * a local infix (name := op) ` ⚬ `:70 := λ a b, a * b + b * a variables {R : Type*} [ring R] diff --git a/test/simps.lean b/test/simps.lean index 6ab8a76833210..74a558af4b53f 100644 --- a/test/simps.lean +++ b/test/simps.lean @@ -421,7 +421,7 @@ example {α β} [semigroup α] [semigroup β] (x y : α × β) : (x * y).1 = x.1 structure Semigroup := (G : Type*) (op : G → G → G) - (infix (name := op) * := op) + (infix (name := op) ` * ` := op) (op_assoc : ∀ (x y z : G), (x * y) * z = x * (y * z)) namespace Group