Zulip Chat Archive

Stream: general

Topic: push_neg


view this post on Zulip Johan Commelin (Feb 08 2020 at 18:19):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Feb 08 2020 at 20:13):

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

view this post on Zulip Johan Commelin (Feb 08 2020 at 20:21):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 08 2020 at 20:21):

simp can simp it away again, afterwards.

view this post on Zulip 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