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).