Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Getting started


view this post on Zulip Bhavik Mehta (May 24 2020 at 14:20):

What's the best way to learn how to write tactics? Is there any documentation or tutorials?

view this post on Zulip Bryan Gin-ge Chen (May 24 2020 at 14:23):

The ones that I know of are https://leanprover-community.github.io/extras/tactic_writing.html and the resources linked there (the metaprogramming paper, the chapters in Programming in Lean) plus the chapters in the "Hitchhiker's guide".

view this post on Zulip Kevin Buzzard (May 24 2020 at 14:23):

Patrick wrote something in the docsextras section of mathlib. You could fix the examples in the Programming In Lean pdf so that they compile :-)

view this post on Zulip Bryan Gin-ge Chen (May 24 2020 at 14:24):

Patrick's tutorial is the one I linked above. We moved most of the "extras" docs out of mathlib and onto the website.

view this post on Zulip Bhavik Mehta (May 24 2020 at 14:26):

The paper is great, I'll have a read of the tutorial too, thanks!

view this post on Zulip Patrick Massot (May 24 2020 at 14:30):

Something that I've been meaning to do forever is to turn the md file into a Lean file with exercises to put into the tutorials project.

view this post on Zulip Patrick Massot (May 24 2020 at 14:30):

I'm sure you could contribute that. There are pretty obvious variations to put in exercises.


Last updated: May 09 2021 at 23:10 UTC