<div dir="auto">Look for uses of next_ml_name in the basis (on my phone, in a rush, sorry)</div><div class="gmail_extra"><br><div class="gmail_quote">On 28 Mar 2017 17:09, "Scott Owens" <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<br>
Scott<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</blockquote></div></div>