Stream: Coq users

Topic: Getting element from `Some`


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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: Feb 06 2023 at 12:04 UTC