coq - 有没有更优雅的方式来编写以下 Coq 代码？

Question

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

我必须这样做很多，嵌套匹配使代码看起来很糟糕。是否有一些更优雅的，一种衬里的方式来解除 Option 的情况？

Answer 1

有option_map函数在 Coq.Init.Datatypes 定义如下:

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.

您可以像评论中显示的@ejgallego 一样使用它: option_map Ref x .

您可以通过以下方式发现此功能:

Search (option _ -> option _).