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

user_8306896 0
Viewed 166
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?

coq
2 Answers

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 _).
user_27475110

More generally, you may want to consider using monadic syntax; it is easy to define some yourself with a couple of Notation declarations, or you can use a more featureful library like Gregory Malecha's ExtLib.

user_83710740
Related