Coqからコードを抽出してコンストラクタのエクスポートを制御する

Question

私はCoqでコードを記述し、このコードを大規模なHaskellプロジェクトで使用することを検討しています。私は、Coqで単一のモジュールを構築し、プロパティを証明し、そしてHaskellのモジュールシステムを使ってこれらのプロパティの違反を防ぐ（スマートコンストラクタ経由で）。

明示的なエクスポートリストを持つHas​​kellモジュールにCoqコードを抽出することはできません。抽出されたCoqコードは手作業で修正する必要があるようですが、それは大きな問題ではありませんが、この権利があるかどうかを知りたいのです。他の誰かが代替案を持っていますか？

Answer 1

最新のcoqソース（r14456）を調べました。エクスポートリストを生成するコードはありません。

あなたはこれを自分で行う必要があるようです。