是否有更优雅的方式来编写以下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 _).

Answer 2

更一般地说,您可能需要考虑使用monadic语法; 使用几个Notation声明很容易定义一些自己,或者你可以使用像Gregory Malecha的ExtLib这样功能更强大的库.