Is there a more elegant way to write the following Coq code?

Question

match x with
| Some x => Some (Ref x)
| None => None
end.

I have to do this quite a lot, nested matches make code look bad. Is there some more elegant, one liner sort of way to lift things out of Option?

Answer 1

There is option_map function in Coq.Init.Datatypes defined as follows:

Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
  match o with
    | Some a => @Some B (f a)
    | None => @None B
  end.

You can use it just like @ejgallego showed in the comments: option_map Ref x.

Here is how you can discover this function:

Search (option _ -> option _).