Zulip Chat Archive

Stream: triage

Topic: issue #2706: rename `squeeze_simp` to `simp?` and have it...


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Feb 12 2021 at 15:51):

I've closed this in favor of #5901.


Last updated: May 18 2021 at 22:15 UTC