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

Question

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

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

Answer 1

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

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