Re: [isabelle] string and altstring
On Thu, 15 Aug 2013, Christian Sternagel wrote:
currently it is possible to write something like "\"" , "\\", `\``, or
`\\` (i.e., there are escape sequences for the delimiters of strings and
altstrings, as well as for backslash).
What many people might be used to from programming languages does not
work however, e.g., "\n", "\t", ...
For that reason we currently have some abbreviations like the following
abbreviation tab :: "char" where
"tab ≡ Char Nibble0 Nibble9"
abbreviation newline :: char where
"newline ≡ Char Nibble0 NibbleA"
abbreviation carriage_return :: "char" where
"carriage_return ≡ Char Nibble0 NibbleD"
abbreviation wspace :: "char list" where
"wspace ≡ CHR '' '' # newline # tab # carriage_return # "
(Maybe there is a better solution?)
Would it make sense to allow the most common escape sequences (like
"\n", "\t", "\r", etc.)? Then I could use
CHR ''\t'', CHR ''\n'', CHR ''\r'', '' \n\t\r''
instead of the above.
Btw: Why does "CHR ''\013''" result in "Char Nibble0 NibbleA"? Shouldn't
that be "Char Nibble0 NibbleD"?
This is off-topic on isabelle-dev ...
The syntax for quoted material in Isabelle deviates in various fine points
from what you see in some other languages, but there were various reasons
to arrive there over many years. I can't recall all of them on the spot.
Any change will inevitably break many things and require years to sort it
out. So as usual there need to be 2-3 really good reasons to consider
that at all.
The standard way to get a line-feed into the HOL term language is indeed
term "CHR ''\010''". It is funny that "CHR ''\013''" also normalizes to
the same -- there are a few more such normalizations built into the notion
of Isabelle symbols, which underlies all text that the prover processes.
Generally, when working with text, especially on top of unicode, there can
be a number of really big surprises. Isabelle avoids most of the dangers
of official Unicode by working with its symbols instead, but this is not
100% bullet proof. We are living in a time where computer systems cannot
process text material reliably and unambigously ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and