Coq的代數類型的OCaml中提取

Question

當我提取下列Coq的數據類型來OCaml的：

Inductive Foo := | A | B. 
Inductive Bar (f:Foo) := | C | D. 
Extraction Language Ocaml. 
Extraction "test.ml" Foo Bar. 

我得到以下ML代碼：

type foo = 
| A 
| B 

type bar = 
| C 
| D 

在「酒吧」型是從不同Coq，因爲它有'f'作爲其類型簽名的一部分。

什麼是最好的方式來定義這些類型，以便它們很好地提取到OCaml？

Answer 1

您不能：OCaml不支持按詞條值編制索引類型，因此諸如Bar A之類的內容對其沒有意義。 Coq被迫刪除額外的索引，以便定義與OCaml的類型系統兼容。