Zulip Chat Archive
Stream: lean4
Topic: Syntax atoms beginning with a single quote
František Silváši (Aug 23 2022 at 14:52):
Is there any way to make: notation "\'" x => x
work? i.e. use '
as the very first character of an atom; or do we always hit the codepath via Lean.Elab.Syntax.isValidAtom
which explicitly prohibits this.
Last updated: Dec 20 2023 at 11:08 UTC