Feature requests/PRs

Stream: new members

[ChiefArug]

I'm using Lean4 to do Advent of Code this year, and I've come across a situation where Option.flatMap (signature of {α β : Type} (f : α → Option β) (o : Option α) : Option β) would be useful. This is a thing in other programming languages (ie Java has its Optional#flatMap) and is analogous to List.flatMap, same as Option.map is analogous to List.map (when list lengths are max 1). I've written my own as you can do, but I think its something that should be in base Lean. What is the process around that, and if I was to make such a PR is there anything else that would need to be added (ie docs, proofs to go along with it, ect). This is a very basic thing so wasn't sure about the whole starting an RFC for it on the GitHub (and that said to ask about it here too anyway).

[Chris Bailey]

This exists as docs#Option.bind, there's a preference for using the names that have come to be associated with the monad typeclass.

[Chris Bailey]

Lean is mature enough that if you're unable to find things of this nature, it's more likely to be a naming thing than a missing implementation.

[ChiefArug]

Ah, thank you. I had tried looking for things around Option.map that had the signature I wanted but didn't manage to find that (looks like it uses the funny match function definition syntax that I still need to wrap my head around).