如何在将Coq提取到Haskell时设置模块名称

Question

当我使用Coq文件中的Extraction Language Haskell.将Coq提取/编译成Haskell并运行coqtop -compile mymodule.v > MyModule.hs时，我得到一个以module Main where开头的Haskell模块。

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

我现在管的sed这样的 -

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

，但我正在寻找一个清晰的解决方案。

Answer 1

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

Definition foo := 6*7. 

Extraction Language Haskell. 
Extraction "MyModule" foo. 

上面产生MyModule.hs文件，其与module MyModule where开始。