Zulip Chat Archive

Stream: new members

Topic: writing tactics - quickstart info


view this post on Zulip Joseph Corneli (Feb 15 2019 at 11:04):

I'm aware of Programming in Lean. Googling just now I found a tech report Meta-programming with the Lean proof assistant. Are there any other guides along these lines for someone starting out writing tactics?

view this post on Zulip Kevin Buzzard (Feb 15 2019 at 11:05):

Didn't Patrick write something in the mathlib docs directory?

view this post on Zulip Kevin Buzzard (Feb 15 2019 at 11:05):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md

view this post on Zulip Kevin Buzzard (Feb 15 2019 at 11:05):

yes

view this post on Zulip Kevin Buzzard (Feb 15 2019 at 11:06):

and that's all I know about.

view this post on Zulip Kevin Buzzard (Feb 15 2019 at 11:06):

or at least all I can remember right now

view this post on Zulip Joseph Corneli (Feb 15 2019 at 11:13):

thanks for the link!


Last updated: May 11 2021 at 13:22 UTC