## Stream: general

### Topic: push_neg

#### Johan Commelin (Feb 08 2020 at 18:19):

Should push_neg also transform \not a = b into a ≠ b?

#### Ryan Lahfa (Feb 08 2020 at 18:32):

Should push_neg also transform \not a = b into a ≠ b?

I just ran into this… :D I was surprised that the transformation was not done, is there any reason?

#### Patrick Massot (Feb 08 2020 at 20:08):

Those are already defeq, but we can still do it if you are sure it would help.

#### Chris Hughes (Feb 08 2020 at 20:13):

¬a=b is simp normal form. \ne should really just be notation not a def.

#### Johan Commelin (Feb 08 2020 at 20:21):

If it's notation, you can no longer write h.symm. But that's minor.

#### Johan Commelin (Feb 08 2020 at 20:21):

I think push_neg is not designed for power users, but for students and beginners. So giving them the ne form is nice.

#### Johan Commelin (Feb 08 2020 at 20:21):

simp can simp it away again, afterwards.

#### Patrick Massot (Feb 08 2020 at 20:23):

I think you PR this and nobody will complain.

Last updated: May 14 2021 at 12:18 UTC