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

Question

当我Extraction Language Haskell.在Coq文件中使用Coq提取/编译Coq到Haskell 并运行时coqtop -compile mymodule.v > MyModule.hs,我得到了一个以Haskell开头的模块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.