Coq Inductive 定义中的 `of` 和 `&` 是什么意思？

Question

我刚刚看到有人用不熟悉的语法在 Coq 中定义了 Inductive 类型，如下所示：

Inductive nat_tree : Type :=
| NatLeaf
| NatNode of color & nat_tree & nat & nat_tree.

我习惯的语法看起来像this:

Inductive ident : sort :=
    ident1  :   type1
|   …        
|   identn  :   typen

谁能解释一下新语法是什么？

顺便说一句，这是来自 ssrflect 教程。我想知道这是不是ssr加法。

Answer 1

是的，你是对的：这个语法是由 Ssreflect 定义的。两者都被定义为用于声明匿名参数的语法糖：of T 和 & T 表示 (_ : T)；也就是说，类型为 T 的未命名参数。因此，nat_tree 的定义等同于下面的定义。

Inductive nat_tree :=
| NatLeaf
| NatNode (_ : color) (_ : nat_tree) (_ : nat) (_ : nat_tree).

您也可以为每个参数命名：

Inductive nat_tree :=
| NatLeaf
| NatNode (c : color) (t1 : nat_tree) (n : nat) (t2 : nat_tree).

正如 gallais 所指出的，这使得 Coq 中数据类型声明的语法更类似于 OCaml 的语法。请注意，上面的声明并没有给出每个构造函数的 return 类型。在标准 Coq 中，当使用此语法给出所有参数时，指定 return 类型是可选的，并且当定义的类型是 uniform 时。这意味着我们可以将 list 类型定义为

Inductive list (T : Type) :=
| nil
| cons (t : T) (l : list T).

但需要按如下方式定义长度索引列表的类型（因为 nat 索引）：

Inductive vector (T : Type) : nat -> Type :=
| vnil : vector T O
| vcons (n : nat) (t : T) (v : vector T n) : vector T (S n).

Coq Inductive 定义中的 `of` 和 `&` 是什么意思？

What's with the `of` and `&` in the Coq Inductive definition?

coq