Coq'den Haskell'e ayıklama yaparken modül adı nasıl ayarlanır

Question

Coq dosyasına Extraction Language Haskell. kullanarak Coq'a Haskell'i ayıkladığım/derlediğimde ve coqtop -compile mymodule.v > MyModule.hs çalıştırdığımda, module Main where ile başlayan bir Haskell modülü alıyorum.

Oluşan Haskell modül adını ayarlamak için bir seçenek var mı?

Şu anda boru

böyle sed -

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

ama temiz bir çözüm arıyorum.

Answer 1

Extraction "file" veya Extraction Library (veya türevlerini), ör.

Definition foo := 6*7. 

Extraction Language Haskell. 
Extraction "MyModule" foo. 

yukarıda module MyModule where ile başlar MyModule.hs dosyası üretir.