Stream: General

Topic: String syntax


view this post on Zulip Lukas Stevens (Jul 14 2021 at 09:17):

Why is ' classified as a special character in string_syntax.ML and therefore not printed as e.g. STR ''won't''?

view this post on Zulip Simon Wimmer (Sep 21 2021 at 16:47):

It has a special meaning as an escape character when you define user-space syntax but I have no idea whether that is related.


Last updated: Dec 07 2024 at 16:22 UTC