Is there a way to get the element inside a `Some`

(constructor of `option`

) in the standard library?

Like to get `3`

out of `Some 3`

or `true`

out of `Some true`

?

In Gallina most people use a match on option values. As far as I know there are no OCaml style helper functions for the Gallina Some. There are such functions for the Ltac2 tactic language Some in (https://github.com/coq/coq/blob/master/user-contrib/Ltac2/Option.v). I would recommend to translate this to Coq into a file Option.v and include this - and maybe do a PR for the standard library. The most interesting question is where one would put such a file since option belongs to Init, but one would not want to have these functions loaded by default.

see here for an overview of approaches: https://plv.csail.mit.edu/blog/unwrapping-options.html

Last updated: Jun 18 2024 at 21:01 UTC