[CakeML-dev] translating i2w

[Ramana Kumar]

I don't think you should translate i2w - can you make your code use
n2w instead? The translator should be able to handle n2w.
(I say this because looking at the translator's hol2deep function I
see it has a case for n2w but not for i2w.)

On 1 December 2016 at 21:44,  <Michael.Norrish at data61.csiro.au> wrote:
> I’m breaking the build on my branch because the parser wants to turn word token integers into word64 values.  I used the i2w constant to do this, but the translator isn’t happy with word_2comp, which is used in this definition. Is there something obvious I should do to fix this?
>
> Or can I use n2w instead by altering the Word token constructor to take a num instead of an int?
>
> Michael
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers