[CakeML-dev] Translator naming questions

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


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


More information about the Developers mailing list