Zulip Chat Archive
Stream: general
Topic: adding to std
Joseph O (Feb 19 2022 at 23:32):
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 (Feb 19 2022 at 23:36):
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 (Feb 19 2022 at 23:38):
Ok, will do
Joseph O (Feb 19 2022 at 23:43):
But there are some I think would be important in the core std
Henrik Böving (Feb 19 2022 at 23:48):
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 (Feb 20 2022 at 01:45):
Ok cool
Joseph O (Feb 20 2022 at 03:08):
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 (Feb 20 2022 at 03:52):
This topic was moved to #mathlib4 > adding to std by Mario Carneiro.
Last updated: Dec 20 2023 at 11:08 UTC