Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Stephan Merz <Stephan.Merz@loria.fr>
Hello,
I recently tried to define constant names that contain backslashes and
ran into a curious behavior of the parser. When I try, say, to declare
(in HOL)
constdefs
"\in" :: "['a, 'a set] => bool" (infixl 50)
"a \in S == a:S"
Isabelle complains about a bad escape character. However, it will
swallow the definition if I write "\\in" (and the output will show
"\in"). Now, when I try to do something similar in Pure, the output will
be "\\in", and the PDF document shows the constant name as ``in.
Should I consider backslashes to be disallowed (as a strict reading of
section 7.2.2 of the reference manual seems to indicate)?
Thanks,
Stephan
Last updated: May 03 2024 at 04:19 UTC