[CakeML-dev] Translator naming questions

Scott Owens S.A.Owens at kent.ac.uk
Tue Mar 28 15:21:36 UTC 2017


Got it.

Scott

> On 2017/03/28, at 16:19, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 
> Look for uses of next_ml_name in the basis (on my phone, in a rush, sorry)
> 
> On 28 Mar 2017 17:09, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:
> How do I use a different CakeML name to the HOL name of a definition in the translator? I have mlstring_lt in HOL, and overload it on <. But I want to translate its definition and add it into the String module in mlstringProgScript.sml with the CakeML name < rather than mlstring_lt.
> 
> Scott
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers




More information about the Developers mailing list