Coq归纳定义中的``和`＆'是什么？

Question

我刚才看到有人在勒柯克在一个陌生的语法定义的感应式，像这样：

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的所指出的，这使得数据类型声明的勒柯克语法更类似于OCaml中的。请注意，上面的声明没有给出每个构造函数的返回类型。在标准Coq中，当使用此语法给出所有参数时，指定返回类型是可选的，并且当定义的类型是统一的时。这意味着，我们被允许定义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).