Option.get

Stream: lean4

[Arthur Paulino]

Do you guys think it's worth adding this one to core?

def Option.get : (a : Option α) → a.isSome → α
  | some a, _ => a

[Jannis Limperg]

I think if you have an isSome proof, you should already have the a. In general, my impression is that PRs which flesh out the API are not super welcome at the moment. So if you need this, I would just stash it into some utility module for now.

[James Gallicchio]

I have the exact same function in my project :joy: is it worth setting up a repo of useful lemmas that aren't in the core? I'd be willing to help maintain one

[James Gallicchio]

(Or is that part of the purpose of mathlib4?)

[Henrik Böving]

That library is called mathlib4 right now indeed. The plan is to eventually phase the generally useful stuff (aka not only mathematics) out into some sort of Stdlib