<div dir="ltr"><div>Hi everyone</div><div><br></div><div>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. <br></div><div><br></div><div>As the error shows, ELECT_Auxiliary_dec is not translatable (the Translation.png file). The screenshot (Encoding Two.png) <br></div><div> shows the definition of the ELECT_Auxiliary_dec.</div><div>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.</div><div><br></div><div>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).</div><div><br></div><div>thanks for your hints,</div><div><br></div><div>Milad<br></div></div>