Как установить имя модуля при извлечении Coq в Haskell

Question

Когда я извлекаю / компилирую Coq в Haskell, используя Extraction Language Haskell. в файле Coq и работает coqtop -compile mymodule.v > MyModule.hsЯ получаю модуль Haskell, который начинается с module Main where,

Есть ли возможность установить получающееся имя модуля Haskell?

Я в настоящее время труба к седу, как это -

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,