控制从 Coq 提取的代码中构造函数的导出
我正在考虑在 Coq 中编写代码并提取此代码以在大型 Haskell 项目中使用。我想在 Coq 中构建单个模块，证明属性，然后使用 Haskell 的模块系统来防止违反这些属性（通过智能构造函数）。
我找不到任何迹象表明可以使用显式导出列表将 Coq 代码提取到 Haskell 模块中。看来我必须手动修改提取的 Coq 代码，这不是什么大问题，但我想知道我是否有这个权利。有人有替代建议吗？
I'm looking at writing code in Coq and extracting this code for use in a large Haskell project. I want to build a single module in Coq, prove properties, then use Haskell's module system to prevent violation of these properties (via smart constructors).
I can't find any indication that it's possible to extract Coq code into a Haskell module with an explicit export list. It seems I must hand-modify the extracted Coq code, which isn't a big deal but I want to know if I have this right. Does anyone have an alternate proposal?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
我刚刚查看了最新的 coq 源代码（r14456）。似乎没有任何代码来生成导出列表。
看来你必须自己做这件事。
I just looked at the latest coq source (r14456). There doesn't seem to be any code to generate an export list.
Seems you'll have to do this yourself.