<div dir="ltr">As you may have seen on Slack, you need to translate `pairTheory.PAIR_MAP` first, because `PART3` uses it.<br></div><br><div class="gmail_quote"><div dir="ltr">On Sun, 9 Dec 2018 at 08:38, Milad Ketabii <<a href="mailto:ketabii.math@gmail.com">ketabii.math@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi There!<div><br></div><div>Unfortunately I have ran into a problem for translating PART3 in SortingTheory from HOL4 to CakeML. </div><div><br></div><div>I was wondering if this problem could be resolved ASAP? I really need this translation to go through. </div><div><br></div><div>many thanks for your guidance,</div><div>Milad</div></div>
_______________________________________________<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>
</blockquote></div>