## Stream: general

### Topic: rw vs simp_rw

#### Johan Commelin (Jul 10 2020 at 03:55):

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 (Jul 10 2020 at 08:44):

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 (Jul 10 2020 at 08:44):

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

#### Patrick Massot (Jul 10 2020 at 08:46):

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

#### Gabriel Ebner (Jul 10 2020 at 08:47):

Anne Baanen said:

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

{single_pass:=tt}

#### Scott Morrison (Jul 10 2020 at 11:07):

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 (Jul 10 2020 at 11:20):

maybe rw_simp can be singlepass and simp_rw multiple pass

#### Kenny Lau (Jul 10 2020 at 11:20):

or better, make rw able to rewrite inside binders

Last updated: May 08 2021 at 10:12 UTC