Tips for writing conversion tactic

Stream: lean4

[Tomas Skrivan]

Is there anything I should look out for when writing conversion tactic? I still do not know how to write such a tactic, but I will look into Lean/Elab/Tactic/Conv/* and Init/Conv.lean, any other place I should look into?

As a start I might add a support for repeat rw [<theorem>], because it does not seem to work in conversion mode.

[Leonardo de Moura]

We have some documentation here: https://leanprover.github.io/theorem_proving_in_lean4/conv.html
I will add a section on writing conv macros. We can do a lot with macros. For more complex tactics, Lean/Elab/Tactic/Conv is the place to look.

[Leonardo de Moura]

I have pushed support for repeat in conv mode.

[Tomas Skrivan]

Yes I have read that section in the doc, it is super useful to get the basic idea about conv, I was wondering where to go beyond.

Thanks a lot for adding a support for repeat.