从Coq提取到Haskell时，是否支持自动添加Haskell导入语句？

好问题！Coq的标准提取功能本身并不直接支持自动添加所需的Haskell导入语句——默认情况下，它只会生成核心的函数/类型定义，不会帮你补上import行。不过你不用急着自己写脚本，Coq其实提供了一些内置机制和社区工具来处理这类需求，不用完全重复造轮子：

• 使用提取注解定制映射：你可以通过Extract Inductive或Extract Constant这类指令，把Coq里的类型/常量映射到Haskell标准库的对应内容。比如把Coq的option类型映射到Haskell的Maybe：

  Extract Inductive option => "Maybe" [ "Nothing" "Just" ].
  

  虽然这不会直接生成导入语句，但它能确保提取后的代码使用标准库的类型，你只需要批量添加对应模块的导入即可，很多场景下可以用简单的模板来完成这一步。
• 借助社区增强工具：社区里有不少针对Coq到Haskell提取的扩展库，它们可以识别提取代码中用到的Haskell标准库类型/函数，自动生成对应的import语句。这些工具基于Coq的提取API封装，已经处理了大部分常见的标准库映射场景，比如自动为list类型添加import Data.List，为Maybe添加import Data.Maybe等。
• 轻量脚本补全（必要时）：如果上述工具不能满足你的定制化需求，Coq提取的代码结构很规整，你可以写几行简单的脚本（比如用Python或Haskell本身）扫描提取后的文件，识别用到的外部模块，自动补全导入语句——但这属于兜底方案，多数时候社区工具已经能覆盖需求。

总的来说，标准提取没有自动导入的原生功能，但借助内置注解和社区工具，你完全不用从零开始写脚本解决问题。

内容的提问来源于stack exchange，提问作者tlon