For the record: this issue has been resolved in http://isabelle.in.tum.de/repos/isabelle/rev/25b431feb2e9.
Cheers, Florian Am 05.09.2018 um 10:32 schrieb Thiemann, René: > Dear all, > > I’m currently changing the error messages in our formalization from the > “string” type to > “String.literal”, so that the exported code uses target language > strings in the generated code. Unfortunately, there seems to be a mistake > in the handling of newline: > > definition "message = STR ''this is⏎a two line text''" > > is translated into Haskell as > > message :: String; > message = "this is\\a two line text"; > > where the \\ should be a \n > > Moreover, also the following behavior is weird: > > lemma "STR ''⏎'' = STR 0x5C" "integer_of_char (CHR ''⏎'') = 10" > by code_simp+ > > Here, one observes that the ''⏎'' gets different characters codes, > depending on whether it is put into a CHR or into a STR. > Note that 0x5C is precisely the backslash as in the generated Haskell code. > > Cheers, > René > > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev