missing delaborator for OreLocalization notation

Stream: mathlib4

[Kevin Buzzard]

import Mathlib.RingTheory.OreLocalization.Ring

variable {R A : Type} [cR : CommSemiring R] [cA : CommSemiring A] [cRA : Algebra R A]
    {S : Submonoid R}

#check A[S⁻¹] -- OreLocalization S A : Type

I still don't know how to write these things :-/

[Kyle Miller]

I think this will do, right after the scoped syntax for the notation in RingTheory.OreLocalization.Basic

open Lean PrettyPrinter in
@[app_unexpander OreLocalization]
private def unexpandOreLocalization : Unexpander
  | `($_ $S $R) => `($R[$S⁻¹])
  | _ => throw ()