जब Coq Haskell को

Question

जब मैं निकालने/संकलन Coq Coq फ़ाइल में Extraction Language Haskell. का उपयोग करने और coqtop -compile mymodule.v > MyModule.hs चल Haskell को निकालने मॉड्यूल का नाम कैसे सेट करें, मैं एक Haskell मॉड्यूल जो module Main where साथ शुरू होता है मिलता है।

क्या परिणामस्वरूप हास्केल मॉड्यूल नाम सेट करने का कोई विकल्प है?

मैं वर्तमान में पाइप इस तरह 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 साथ शुरू होता है पैदा करता है।