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

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sun Dec 9 08:50:03 UTC 2018


As you may have seen on Slack, you need to translate `pairTheory.PAIR_MAP`
first, because `PART3` uses it.

On Sun, 9 Dec 2018 at 08:38, Milad Ketabii <ketabii.math at gmail.com> wrote:

> 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,
> Milad
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20181209/fd0055a2/attachment.html>


More information about the Users mailing list