控制从Coq中提取的代码中构造函数的导出

Question

我正在考虑在Coq中编写代码并提取此代码以用于大型Haskell项目.我想在Coq中构建一个单独的模块,证明属性,然后使用Haskell的模块系统来防止违反这些属性(通过智能构造函数).

我找不到任何迹象表明可以将Coq代码提取到具有显式导出列表的Haskell模块中.看来我必须手工修改提取的Coq代码,这不是什么大问题,但我想知道我是否有这个权利.有人有替代提案吗？

Answer 1

我刚刚查看了最新的 coq 源代码（r14456）。似乎没有任何代码来生成导出列表。

看来你必须自己做这件事。