<div dir="ltr">Hi There!<div><br></div><div>Already I came up with a solution ofr the ELECT_Auxiliary_dec problem. However, I would be very much thankful if someone let me know about the TRANSFER_Auxiliary (screenshot Encoding_FOUR.png).</div><div><br></div><div>It would also be great if someone had an explanation as why the let binding in the ELECT_Auxiliary_dec is the criminal (I personally have no idea).</div><div><br></div><div>thanks,</div><div>Milad</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Dec 10, 2018 at 8:30 PM <<a href="mailto:users-request@cakeml.org">users-request@cakeml.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Send Users mailing list submissions to<br>
        <a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a><br>
<br>
To subscribe or unsubscribe via the World Wide Web, visit<br>
        <a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
or, via email, send a message with subject or body 'help' to<br>
        <a href="mailto:users-request@cakeml.org" target="_blank">users-request@cakeml.org</a><br>
<br>
You can reach the person managing the list at<br>
        <a href="mailto:users-owner@cakeml.org" target="_blank">users-owner@cakeml.org</a><br>
<br>
When replying, please edit your Subject line so it is more specific<br>
than "Re: Contents of Users digest..."<br>
<br>
<br>
Today's Topics:<br>
<br>
   1.  New problems in Translation again! (Milad Ketabii)<br>
<br>
<br>
----------------------------------------------------------------------<br>
<br>
Message: 1<br>
Date: Mon, 10 Dec 2018 19:19:51 +1100<br>
From: Milad Ketabii <<a href="mailto:ketabii.math@gmail.com" target="_blank">ketabii.math@gmail.com</a>><br>
To: <a href="mailto:users@cakeml.org" target="_blank">users@cakeml.org</a><br>
Subject: [CakeML] New problems in Translation again!<br>
Message-ID:<br>
        <<a href="mailto:CAFLPSnwUkppTZP_Pn3paU_Db2tfyb5mUYwj17VBjvaC-RG6XWA@mail.gmail.com" target="_blank">CAFLPSnwUkppTZP_Pn3paU_Db2tfyb5mUYwj17VBjvaC-RG6XWA@mail.gmail.com</a>><br>
Content-Type: text/plain; charset="utf-8"<br>
<br>
Hi everyone<br>
<br>
Attached are three screen shots that show the encoding of what i want to<br>
translate from HOL4 to CakeML and the error that I get.<br>
<br>
As the error shows, ELECT_Auxiliary_dec is not translatable (the<br>
Translation.png file). The screenshot (Encoding Two.png)<br>
 shows the definition of the ELECT_Auxiliary_dec.<br>
Once i rewrite the ELECT_Auxiliary into another function (screenshot<br>
EncodingThree,png) the translation goes OK. How can I fix the problem with<br>
ELECT_Auxiliary_dec so that it becomes translatable. I do not want to<br>
compute some functions several times so the let binding is important.<br>
<br>
The file Encoding_Four,png shows more or less the same problem with another<br>
definition; once I include it in a pattern match environment, the<br>
translation goes through. How can I get it translated as it is in the<br>
screenshot (or with some modifications).<br>
<br>
thanks for your hints,<br>
<br>
Milad<br>
-------------- next part --------------<br>
An HTML attachment was scrubbed...<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.html" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.html</a>><br>
-------------- next part --------------<br>
A non-text attachment was scrubbed...<br>
Name: Translation.png<br>
Type: image/png<br>
Size: 194030 bytes<br>
Desc: not available<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.png" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment.png</a>><br>
-------------- next part --------------<br>
A non-text attachment was scrubbed...<br>
Name: Encoding_ScreenOne.png<br>
Type: image/png<br>
Size: 200838 bytes<br>
Desc: not available<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0001.png" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0001.png</a>><br>
-------------- next part --------------<br>
A non-text attachment was scrubbed...<br>
Name: Encoding_ScreenTwo.png<br>
Type: image/png<br>
Size: 174523 bytes<br>
Desc: not available<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0002.png" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0002.png</a>><br>
-------------- next part --------------<br>
A non-text attachment was scrubbed...<br>
Name: Encoding_ScreenThree.png<br>
Type: image/png<br>
Size: 159649 bytes<br>
Desc: not available<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0003.png" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0003.png</a>><br>
-------------- next part --------------<br>
A non-text attachment was scrubbed...<br>
Name: Encoding_Four.png<br>
Type: image/png<br>
Size: 94083 bytes<br>
Desc: not available<br>
URL: <<a href="https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0004.png" rel="noreferrer" target="_blank">https://lists.cakeml.org/pipermail/users/attachments/20181210/f417f5b5/attachment-0004.png</a>><br>
<br>
------------------------------<br>
<br>
Subject: Digest Footer<br>
<br>
_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br>
<br>
------------------------------<br>
<br>
End of Users Digest, Vol 28, Issue 3<br>
************************************<br>
</blockquote></div>