Zulip Chat Archive
Stream: triage
Topic: issue #3273: squeeze_simp also simplify targets
Random Issue Bot (Apr 12 2022 at 14:13):
Today I chose issue 3273 for discussion!
squeeze_simp also simplify targets
Created by @Alex J Best (@alexjbest) on 2020-07-03
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Alex J. Best (Apr 12 2022 at 14:18):
I still think this would be useful for minifying simp [*] at * type proofs, in fact I would have found it very helpful just yesterday.
Yaël Dillies (Apr 12 2022 at 14:19):
The problem is that simp h at h turns h : p into h : true :sad:
Alex J. Best (Apr 12 2022 at 14:25):
That's not a problem for simp [*] at *, it has a special implementation to avoid this
Random Issue Bot (May 01 2022 at 14:20):
Today I chose issue 3273 for discussion!
squeeze_simp also simplify targets
Created by @Alex J Best (@alexjbest) on 2020-07-03
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 08 2022 at 14:15):
Today I chose issue 3273 for discussion!
squeeze_simp also simplify targets
Created by @Alex J Best (@alexjbest) on 2020-07-03
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 30 2023 at 14:09):
Today I chose issue 3273 for discussion!
squeeze_simp also simplify targets
Created by @Alex J Best (@alexjbest) on 2020-07-03
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 10 2023 at 14:09):
Today I chose issue 3273 for discussion!
squeeze_simp also simplify targets
Created by @Alex J Best (@alexjbest) on 2020-07-03
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC