Learning lean macros

Stream: lean4

[Joseph O]

So I wanted to create my own custom syntax to define functions, but I didn't really know how to do it. So I looked at alloy for examples, but I wasn't able to understand anything. How were they able to learn how to use macros, and how can I?

[Arthur Paulino]

Porting some tactics to mathlib4 is teaching me wonders

[Chris B]

Parts 11.4 and 11.5 in the manual are good, and mathlib4's tactic/basic has some examples.

[Andrés Goens]

there's a nice tutorial also hidden on the docs: https://github.com/leanprover/lean4/blob/master/doc/tutorial/metaprogramming-arith.md

[Joseph O]

Andrés Goens said:

there's a nice tutorial also hidden on the docs: https://github.com/leanprover/lean4/blob/master/doc/tutorial/metaprogramming-arith.md

Oh interesting

[Adrien Champion]

Now available at https://leanprover.github.io/lean4/doc/metaprogramming-arith.html

[Adrien Champion]

Has there been new, potentially more in-depth material for learning macros published somewhere?

[Leonardo de Moura]

https://arxiv.org/pdf/2001.10490.pdf

[Adrien Champion]

I did read this paper, which helped a great deal, but I was hoping for something more hands-on

[Adrien Champion]

This seems to fit the bill: https://github.com/arthurpaulino/lean4-metaprogramming-book

[Adrien Champion]

Arthur Paulino said:

Porting some tactics to mathlib4 is teaching me wonders

Seems like it really did, thank you for this book!

[Arthur Paulino]

The book is the result of a big collaborative effort. I, alone, didn't write much