Zulip Chat Archive

Stream: lean4

Topic: Tips for writing conversion tactic


Tomas Skrivan (Oct 06 2021 at 05:30):

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 (Oct 06 2021 at 20:59):

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 (Oct 06 2021 at 21:08):

I have pushed support for repeat in conv mode.

Tomas Skrivan (Oct 07 2021 at 08:22):

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.


Last updated: Dec 20 2023 at 11:08 UTC