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 2023 at 08:19 UTC