## Stream: general

### Topic: ge/gt as a notation?

#### Yury G. Kudryashov (Mar 24 2020 at 19:42):

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 (Mar 24 2020 at 19:44):

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

Last updated: May 14 2021 at 12:18 UTC