Zulip Chat Archive
Stream: triage
Topic: issue #3428: library_search and negation
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?
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?
Patrick Massot (Nov 03 2020 at 20:03):
No, it's not, see the issue. Sorry about forgetting about this issue.
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?
Patrick Massot (Dec 27 2020 at 14:29):
Yes, it's still relevant. And I'd love to learn that someone is making progress.
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
Bhavik Mehta (Dec 27 2020 at 15:00):
iirc ne.def is a simp lemma so \not x = y is simp-normal
Random Issue Bot (Nov 12 2021 at 14:19):
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?
Random Issue Bot (Jan 08 2022 at 14:16):
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?
Last updated: Dec 20 2023 at 11:08 UTC