Is there a way to get the element inside a
Some (constructor of
option) in the standard library?
Like to get
3 out of
true out of
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: Feb 06 2023 at 12:04 UTC