Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: Getting started
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?
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".
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 :-)
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.
Bhavik Mehta (May 24 2020 at 14:26):
The paper is great, I'll have a read of the tutorial too, thanks!
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.
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: Dec 20 2023 at 11:08 UTC