Zulip Chat Archive
Stream: mathlib4
Topic: scoped notation3
Patrick Massot (Nov 01 2023 at 14:14):
@Kyle Miller it seems you cannot write scoped[MyNameSpace] notation3. Is this is a known issue? Is there another syntax?
Kyle Miller (Nov 01 2023 at 18:03):
Patrick Massot (Nov 01 2023 at 19:45):
Amazing, thanks!
Patrick Massot (Nov 01 2023 at 19:46):
In case you wonder, the context of my question was https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/request.20for.20help.20with.20filter.20notation/near/399647325. There was some scoped notation that needed a fix, and I wanted to use notation3 to get a delaborator for free.
Patrick Massot (Nov 01 2023 at 19:48):
Oh I see that you participated in the GitHub discussion so you probably figured out this context.
Last updated: Dec 20 2023 at 11:08 UTC