[CakeML] Reporting translation problem for "PART3" in sortingTheory
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,
> Users mailing list
> Users at cakeml.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Users