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