Stream: metaprogramming / tactics
Topic: Lean Best Practices
Alena Gusakov (May 22 2020 at 16:43):
So I don't know if this is best place to post this but I'm wondering if there are some sorts of informal style guidelines people like to follow for Lean? Best ways of writing definitions/proofs, that sort of thing. It seems like there are multiple ways of writing Lean proofs, which is true of regular math proofs too, but I wonder if there's more to it on the Lean side of things
Markus Himmel (May 22 2020 at 16:49):
Alena Gusakov (May 22 2020 at 16:52):
Ah, neat! Thank you!
Jalex Stark (May 22 2020 at 16:54):
by the way "metaprogramming" refers to writing code that involves the
meta keyword. This is how things like
ring are written.
Kevin Buzzard (May 22 2020 at 17:34):
At the Xena project we don't have any style guidelines -- if it compiles, you won.
Scott Morrison (May 23 2020 at 02:33):
But those are just the introductory levels. When Xena advances to the boss levels (getting PRs merged in mathlib) it helps to have practice with the right techniques. :-)
Bhavik Mehta (May 23 2020 at 03:13):
Can confirm getting PRs merged and making the linter happy is the real boss fight of lean
Scott Morrison (May 23 2020 at 05:15):
Beyond that there's reviewing other people's PRs, and beyond that, convincing all the bright young things doing lovely maths in Lean to put in the effort to PR it all! :-)
Kevin Buzzard (May 23 2020 at 07:19):
My take on it is that one way to find 5 people who will take it seriously and make good PRs is to tell 500 people about Lean
Kevin Buzzard (May 23 2020 at 07:20):
I am not sure I am capable of teaching things like good coding practice because at the end of the day I am not actually a good computer scientist
Last updated: May 09 2021 at 22:13 UTC