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

Question

当我使用 Extraction Language Haskell. 提取/编译 Coq 到 Haskell 时在 Coq 文件中并运行 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 开头.