coq中的“Some”是什么意思？

Question

coq 中的关键字/命令“Some”是什么意思？

此外，我如何查看它的定义？考虑到some 这个词的流行度，使用coq some 并没有太大帮助。

Answer 1

Some 是option 类型的类型构造函数。您可以通过Checking 或Printing 获取有关此类构造函数的一些信息，以获取它们的类型或完整实现。

编辑：option 类型是什么。

它是 Coq 前奏中定义的类型（同样，使用 Check 或 Print 获取有关此类型的信息）。该类型用于陈述关于可选存在类型的事实：对于任何类型A，None : option A 表示没有值，Some A: option A 表示存在值（类型为A）。

这是一个自然数前身的例子：

Definition myPred (n:nat) : option nat := match n with
  | S p => Some p
  | O => None
end.

在本例中，如果您尝试计算O 的前任，您将得到None（没有这样的自然数）。否则，你会得到Some p 这样S p = n。