Zulip Chat Archive

Stream: general

Topic: symmetry


view this post on Zulip Kevin Buzzard (Jul 04 2019 at 17:14):

The symmetry tactic won't turn a ≠ b into b ≠ a (at least it won't for my home-grown nats). This can be fixed with

attribute [symm] ne.symm

Unfortunately ne.symm is in core so it's not so easy to tag it with this attribute. Is there a place in mathlib where this line could go?

view this post on Zulip Johan Commelin (Jul 04 2019 at 17:20):

data/logic.lean?

view this post on Zulip Johan Commelin (Jul 04 2019 at 17:21):

That's imported by almost everything else, and it seems a fitting place.


Last updated: May 13 2021 at 05:21 UTC