Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] backslashes in constant names

view this post on Zulip 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: Nov 21 2024 at 12:39 UTC