idris-lang/Idris-dev — pull request #694 by ahmadsalim (2013-11-30 15:54:49+00:00)
Title: Support unicode characters for operators

We already support Unicode for identifiers, this would allow defining operators as Unicode too. There should probably be a flag in the future to disable Unicode support entirely (but that will take some time to implement, where this was a one-liner).