Zulip Chat Archive

Stream: new members

Topic: Hello + adding list lemmas

Ethan Pronovost (Oct 17 2021 at 16:03):

Hello! I'm new to Lean. As part of a personal project, I've written a few more lemmas about properties of lists that weren't already in mathlib (as far as I could tell). They all fit the general description of "some property about combining 2 or more list methods". For example

lemma head'_append {α : Type*} {l₁ l₂ : list α} {x : α} (h : x  l₁.head') :  x  (l₁ ++ l₂).head' := ...

Would these sorts of contributions be welcomed in a PR?

Anne Baanen (Oct 18 2021 at 10:21):

Welcome! New lemmas that you needed for some project are almost always appreciated, so please make your PR! In fact, I'm not aware of any file where we claim the collection of lemmas is complete and quite a few where the opposite holds.

Ethan Pronovost (Oct 20 2021 at 05:38):

Cool! Can I request to have write access to non-master branches of the mathlib repository as per the instructions here?

Johan Commelin (Oct 20 2021 at 05:40):

@Ethan Pronovost what is your github username?

Ethan Pronovost (Oct 21 2021 at 04:18):

@Johan Commelin EPronovost

Scott Morrison (Oct 21 2021 at 04:25):


Ethan Pronovost (Oct 22 2021 at 04:07):


Last updated: Dec 20 2023 at 11:08 UTC