adding to std

Stream: general

[Joseph O]

Im currently working on a package that is meant to expand on lean's current std for lists, but I started considering whether I should add them to lean's std directly. I would like some input. Thank in advance, and also, here is the current repo

[Mario Carneiro]

My suggestion is to add to mathlib4, for example here -> https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/List/Defs.lean

[Joseph O]

Ok, will do

[Joseph O]

But there are some I think would be important in the core std

[Henrik Böving]

the compiler Std's purpose is to contain everything that the compiler needs to build itself that doesn't fit in other packages, everything else goes to mathlib 4 for now and will probably find a new home in some "std-ext" or whatever at some point.

[Joseph O]

Ok cool

[Joseph O]

Im pretty new to this, so I want to ask. Is this an ok docstring?

/--
`List.choose` filters list `l` of type `List α` with `chooser` which is of type `α → Option β`
It keeps the elements where `chooser x` is `some _` and discards the ones that are `none`

Example:
```
def oneTwo? : Nat → Option Nat
  | 1 => some 1
  | 2 => some 2
  | _ => none

[1, 2, 3, 5, 1, 4, 2] |> choose oneTwo? = [1, 2, 1, 2]
```
-/

[Notification Bot]

This topic was moved to #mathlib4 > adding to std by Mario Carneiro.