[CakeML] New problems in Translation again!

[Milad Ketabii]

Hi everyone

Attached are three screen shots that show the encoding of what i want to
translate from HOL4 to CakeML and the error that I get.

As the error shows, ELECT_Auxiliary_dec is not translatable (the
Translation.png file). The screenshot (Encoding Two.png)
 shows the definition of the ELECT_Auxiliary_dec.
Once i rewrite the ELECT_Auxiliary into another function (screenshot
EncodingThree,png) the translation goes OK. How can I fix the problem with
ELECT_Auxiliary_dec so that it becomes translatable. I do not want to
compute some functions several times so the let binding is important.

The file Encoding_Four,png shows more or less the same problem with another
definition; once I include it in a pattern match environment, the
translation goes through. How can I get it translated as it is in the
screenshot (or with some modifications).

thanks for your hints,

Milad
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Translation.png
Type: image/png
Size: 194030 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0005.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Encoding_ScreenOne.png
Type: image/png
Size: 200838 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0006.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Encoding_ScreenTwo.png
Type: image/png
Size: 174523 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0007.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Encoding_ScreenThree.png
Type: image/png
Size: 159649 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0008.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Encoding_Four.png
Type: image/png
Size: 94083 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0009.png>