rw vs simp_rw

Stream: general

[Johan Commelin]

Are there downsides to using simp_rw vs rw? Is simp_rw going to be (much) slower? Otherwise I wonder if they should be merged.

[Anne Baanen]

There are things that simp_rw can't do by default: if your rewrite equation looks like x = some_function_of x then simp_rw is going to loop

[Anne Baanen]

There is presumably some fancy configuration that we can pass to simp to prevent this

[Patrick Massot]

Even without looping you sometimes want to rewrite only one occurence of a pattern.

[Gabriel Ebner]

Anne Baanen said:

There is presumably some fancy configuration that we can pass to simp to prevent this

{single_pass:=tt}

[Scott Morrison]

Could we turn on single_pass by default in simp_rw? This often trips me up, and I don't ever rely on the current behaviour (although presumably places in mathlib do at this point)

[Kenny Lau]

maybe rw_simp can be singlepass and simp_rw multiple pass

[Kenny Lau]

or better, make rw able to rewrite inside binders