[CakeML] Reporting translation problem for "PART3" in sortingTheory

Milad Ketabii ketabii.math at gmail.com
Sun Dec 9 03:21:52 UTC 2018

Hi There!

Unfortunately I have ran into a problem for translating PART3 in
SortingTheory from HOL4 to CakeML.

I was wondering if this problem could be resolved ASAP? I really need this
translation to go through.

many thanks for your guidance,
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181209/767ff7c2/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TransLationProblem.png
Type: image/png
Size: 89419 bytes
Desc: not available
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181209/767ff7c2/attachment-0001.png>

More information about the Users mailing list