fix: OreLocalization notation breaks [] (#4267)

As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Bug.2FObservation.20about.20Empty.20Lists/near/360479548).
leanprover-community · May 31, 2023 · 6007b4d · 6007b4d
1 parent 53e068c
commit 6007b4d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -85,9 +85,9 @@ variable {R : Type _} [Monoid R] {S : Submonoid R}
 
 variable (R S) [OreSet S]
 
--- mathport name: «expr [ ⁻¹]»
 @[inherit_doc OreLocalization]
-notation:1075 R "[" S "⁻¹]" => OreLocalization R S
+scoped syntax:1075 term noWs atomic("[" term "⁻¹" noWs "]") : term
+macro_rules | `($R[$S⁻¹]) => ``(OreLocalization $R $S)
 
 attribute [local instance] oreEqv