When I last looked at this -- admittedly years ago at this point -- all Unicode operators had an ASCII alternative. So maybe you could enter the code as Ascii a

When I last looked at this -- admittedly years ago at this point -- all Unicode operators had an ASCII alternative. So maybe you could enter the code as Ascii and prettify it into Unicode?