如何在將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開始。