Allow unicode in operators

[mikeshulman]

The syntax for binary operators would be a lot more useful if the operator could include unicode characters.

[andrejbauer]

The ideal solution is the mix-fix notation of Agda. In the meanwhile, it's easy enough to create new infix binary operators, if someone tells us which ones.

[mikeshulman]

Could you just do all the math symbols?