adding to std

Stream: mathlib4

[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]
```
-/

[Yakov Pechersky]

Can you explain what the beta type does? Does it map to it or ignore the beta value? Your oneTwo? is a version of id, so it's hard to tell.

[Mario Carneiro]

l.choose f = l.filter (f · |>.isSome), so I'm not sure it's a really worthwhile function

[Notification Bot]

This topic was moved here from #general > adding to std by Mario Carneiro.

[Mario Carneiro]

the name is also easily confused with other uses of "choose" or "choice" in mathlib, like docs#fintype.choose or docs#nat.choose

[Reid Barton]

From the example the behavior could also be filter_map.

[Joseph O]

Mario Carneiro said:

l.choose f = l.filter (f · |>.isSome), so I'm not sure it's a really worthwhile function

I guess you are right

[Joseph O]

I have found it useful once or twice, when filtering does out a list with a function that returns option

[Joseph O]

Yakov Pechersky said:

Can you explain what the beta type does? Does it map to it or ignore the beta value? Your oneTwo? is a version of id, so it's hard to tell.

I would say that it is ignored

[Yakov Pechersky]

That detail is probably good to include in your docstring. Think of the docstring as the specification for your code. Of course, there's always the source code itself, but that might change over time as you discover you have to deal ith certain implementation details. But the docstring, especially for such an API function, would likely remain constant.

[Joseph O]

Ok, thanks

[Joseph O]

Do you think this is better?

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

[Joseph O]

And also, is it just me or does docgen-4 have support for docstrings now?

[Henrik Böving]

Yes it does