Email Gateway (Aug 22 2022 at 13:36): Email Gateway (Aug 22 2022 at 13:36):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
Why do I get the type "nibble" for the attached file?
Thanks,
Jørgen
Scratch.thy
Email Gateway (Aug 22 2022 at 13:36):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jørgen,
The char type is defined in HOL as a pair of nibbles, and String.literal in terms of lists
of characters. For code generation, String.literal is mapped to strings in the target
language, but this happens only after the code generator has gone over the internal
construction of types. So it does not realise that nibble is not needed at all.
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 13:38):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks for the explanation. I guess it cannot be changed then. :-)
Jørgen
Last updated: Apr 25 2024 at 20:15 UTC