Zulip Chat Archive
Stream: triage
Topic: issue #2706: rename `squeeze_simp` to `simp?` and have it...
Random Issue Bot (Feb 03 2021 at 14:22):
Today I chose issue 2706 for discussion!
rename squeeze_simp to simp? and have it also output a rewrite trace (if possible)
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2020-05-17
Labels: feature-request, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Feb 03 2021 at 14:23):
Partial progress has been made. simp? is now available, but not all features of squeeze_simp have been ported yet.
Random Issue Bot (Feb 12 2021 at 14:20):
Today I chose issue 2706 for discussion!
rename squeeze_simp to simp? and have it also output a rewrite trace (if possible)
Created by @Bryan Gin-ge Chen (@bryangingechen) on 2020-05-17
Labels: feature-request, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Bryan Gin-ge Chen (Feb 12 2021 at 15:51):
I've closed this in favor of #5901.
Last updated: Dec 20 2023 at 11:08 UTC