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的类型系统兼容。