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 ( 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:

Last updated: Sep 23 2023 at 14:01 UTC