Making small contributions to Lean4/Mathlib

Stream: new members

[Craig McLaughlin]

According to: https://leanprover-community.github.io/contribute/index.html, I'm advised to ask for write access to the Mathlib repo in preparation for any contributions I will make. At the moment, I have some small additions regarding Lists (lemmas about permutations) that would be better placed in the lean4 repo. Is the process the same? Or should I create my own fork and submit pull requests from there?

Edit: My github username is cmcl

[Jireh Loreaux]

The process for the lean4 repo is not the same. Can you specify what small additions you are interested to make regarding List? Knowing what they are could help us direct you better (either pointing you to API that already exists, or telling you how to interact with the lean4 repo appropriately).

[Craig McLaughlin]

One lemma I had in mind (from my own need in a personal project): I wish to decompose List.filter p l assumptions such that there exists l1 and l2 where l1 ++ l2 is a permutation of l and p is true of all l1 and not . p is true of all l2. (It only occurred to me today that Perm was recently moved into lean4 from Batteries).

[Craig McLaughlin]

Of course, I am happy to fork and submit a pull request as well if write access to lean4 is more tightly controlled.

[Violeta Hernández]

Lean 4 has very different standards than Mathlib, and contributing to it is much harder. If you're a beginner, I'm 99% confident you should be contributing to Mathilb instead.

[Eric Wieser]

Regarding your example, you might be looking for docs#List.partition