Julin S (Nov 20 2021 at 04:48): Julin S (Nov 20 2021 at 04:48):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 3or true out of Some true?
Michael Soegtrop (Nov 20 2021 at 09:26):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.
Karl Palmskog (Nov 21 2021 at 14:03):see here for an overview of approaches: https://plv.csail.mit.edu/blog/unwrapping-options.html
Last updated: Sep 23 2023 at 14:01 UTC