Zulip Chat Archive

Stream: new members

Topic: replace simp with the rewrites it used


view this post on Zulip Ariel Fridman (Feb 18 2021 at 16:23):

Sometimes I use simp in the middle of a proof, which I know is a bad thing but it can be very useful in certain situations.

Is there an easy way to replace it with the rewrites it ran, except of setting trace.simplify.rewrite to true and copying the steps manually?

view this post on Zulip Ruben Van de Velde (Feb 18 2021 at 16:23):

squeeze_simp

view this post on Zulip Ariel Fridman (Feb 18 2021 at 16:24):

Ruben Van de Velde said:

squeeze_simp

ooh, that's useful. Thank you! ^^


Last updated: May 16 2021 at 05:21 UTC