fix: at notation for ProjectiveSpectrum.StructureSheaf (#5758)

Switches to `notation3` and eliminates dot notation so it can generate a pretty printer.
leanprover-community · Jul 7, 2023 · 88e1297 · 88e1297
1 parent 38b0bb0
commit 88e1297
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
@@ -65,8 +65,9 @@ variable [CommRing R] [CommRing A] [Algebra R A]
 
 variable (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜]
 
-local macro "at " x:term : term => `(HomogeneousLocalization.AtPrime 𝒜
-  ($x : ProjectiveSpectrum.top 𝒜).asHomogeneousIdeal.toIdeal)
+local notation3 "at " x =>
+  HomogeneousLocalization.AtPrime 𝒜
+    (HomogeneousIdeal.toIdeal (ProjectiveSpectrum.asHomogeneousIdeal x))
 
 namespace ProjectiveSpectrum.StructureSheaf