haskell - 从 Coq 中提取时可以自动添加 Haskell 导入语句吗？

Question

我正在从 Coq 提取到 Haskell，这需要在 Haskell 端导入几个模块。是否有任何 Coq 提取功能可以让您自动执行此操作？我知道我可以写一个脚本来做到这一点，但如果有必要我宁愿不要重新发明轮子。

Answer 1

没有，非常难过。

我们已经通过添加多个导入（ fiximports.py ）的 Python 脚本解决了这个问题，但这需要使用 Haskell 预处理器（您通过传递-F -pgmF fiximports.pyto 来使用它ghc）并导致未使用的导入警告，并且不是非常优雅。

我认为问题在于这些导入对于 OCaml 提取是不必要的，并且尚未为 Haskell 提取设计和实现该功能。