notation3 issue

Stream: mathlib4

[Patrick Massot]

Does anyone know how to fix the warning in

import Mathlib.Topology.NhdsSet

open Topology

notation3 "∀ᶠ " (...) " near "s", "r:(scoped p => Filter.Eventually p <| 𝓝ˢ s) => r

[Kyle Miller]

#6833 should let it work as-is

In the meantime, notation3 doesn't support notation in its expansions if you want to generate a pretty printer:

notation3 "∀ᶠ " (...) " near "s", "r:(scoped p => Filter.Eventually p <| nhdsSet s) => r

[Kyle Miller]

(I just checked. #6833 does indeed fix the warning.)

[Patrick Massot]

Thanks!