Zulip Chat Archive

Stream: triage

Topic: issue #3428: library_search and negation


view this post on Zulip Random Issue Bot (Nov 03 2020 at 14:14):

Today I chose issue 3428 for discussion!

library_search and negation
Created by @Patrick Massot (@PatrickMassot) on 2020-07-17
Labels: enhancement, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Rob Lewis (Nov 03 2020 at 14:16):

@Scott Morrison @Patrick Massot apparently this works now with library_search!. Do we think that's enough?

view this post on Zulip Patrick Massot (Nov 03 2020 at 20:03):

No, it's not, see the issue. Sorry about forgetting about this issue.

view this post on Zulip Random Issue Bot (Dec 27 2020 at 14:27):

Today I chose issue 3428 for discussion!

library_search and negation
Created by @Patrick Massot (@PatrickMassot) on 2020-07-17
Labels: enhancement, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Patrick Massot (Dec 27 2020 at 14:29):

Yes, it's still relevant. And I'd love to learn that someone is making progress.

view this post on Zulip Kevin Buzzard (Dec 27 2020 at 14:58):

What's the simp normal form for \not x = y? I try to avoid ever making such terms eg I might case on eq_or_ne a b rather than casing on a=b

view this post on Zulip Bhavik Mehta (Dec 27 2020 at 15:00):

iirc ne.def is a simp lemma so \not x = y is simp-normal


Last updated: May 09 2021 at 16:20 UTC