Showing intermediate 'simp/rw' state in the infoview

Stream: general

[Aaron Hill]

When reading through a long 'rw' or 'simp only' statement, I often break up the statement into several smaller ones (e.g. rw [hA, hB] to rw [ha]; rw [hb] so that I can see the effect of each rule on the target goal/hypothesis in the infoview.

It would be useful to be able to do this by just moving the cursor around in the original 'rw/simp only' statement. My understanding is that this would require the simp and rw syntax/tactics to have some kind of integration with the lean LSP server, which would allow them to add extra detail to LSP responses when the cursor is within their range of tokens. Does anything like this currently exist?

[Etienne Marion]

This already works with rw.

[Joachim Breitner]

And for simp it's probably not doable, as it doesn't apply these lemmas in order.

[Ruben Van de Velde]

You can use simp_rw instead

[Aaron Hill]

Thanks - not sure how I missed that this works for rw

[Joachim Breitner]

Probably because it's almost too good to be true :-)