Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC