haskell - Coq解压到Haskell时如何设置模块名

Question

当我在 Coq 文件中提取/编译 Coq 到 HaskellExtraction Language Haskell.并运行coqtop -compile mymodule.v > MyModule.hs时，我得到一个以module Main where.

是否有设置生成的 Haskell 模块名称的选项？

我目前像这样通过管道传输到 sed -

coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs

但我正在寻找更清洁的解决方案。

Answer 1

您可以使用Extraction "file"or Extraction Library（或其变体），例如

Definition foo := 6*7.

Extraction Language Haskell.
Extraction "MyModule" foo.

以上生成MyModule.hs文件，该文件以module MyModule where.