Re: [isabelle] Question about code generation



Thanks for the explanation. I guess it cannot be changed then. :-)

Jørgen

-----Original Message-----
From: Andreas Lochbihler [mailto:andreas.lochbihler at inf.ethz.ch] 
Sent: 15. juni 2016 08:37
To: Jørgen Villadsen; cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Question about code generation

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

On 14/06/16 18:57, Jørgen Villadsen wrote:
> Hi,
>
> Why do I get the type "nibble" for the attached file?
>
> Thanks,
>
> Jørgen
>




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.