Zulip Chat Archive
Stream: triage
Topic: issue #5901: simp? and squeeze_simp
Random Issue Bot (Oct 14 2021 at 14:19):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Oct 14 2021 at 14:55):
I guess this is wontfix with Lean 4 around the corner.
Random Issue Bot (Oct 29 2021 at 14:19):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 26 2021 at 14:19):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 01 2022 at 14:28):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 17 2022 at 14:39):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 11 2022 at 14:08):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 14 2023 at 14:09):
Today I chose issue 5901 for discussion!
simp? and squeeze_simp
Created by @Johan Commelin (@jcommelin) on 2021-01-26
Labels: t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Jan 14 2023 at 14:45):
wontfix, I guess?
Johan Commelin (Jan 14 2023 at 14:46):
In Lean 4, the whole thing is moot
Yaël Dillies (Jan 15 2023 at 14:12):
Yeah, I think we can just close it.
Last updated: Dec 20 2023 at 11:08 UTC