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