ge/gt as a notation?

Stream: general

[Yury G. Kudryashov]

Would it be bad to have a > b as a notation instead of a def? Then we can stop worrying about a < b or b > a.

[Gabriel Ebner]

lean#152 But @Simon Hudon doesn't like it and would prefer to change the simplifier instead.