Cách đặt tên mô-đun khi trích xuất Coq thành Haskell

Question

Khi tôi trích xuất/biên dịch Coq thành Haskell bằng cách sử dụng Extraction Language Haskell. trong tệp Coq và chạy coqtop -compile mymodule.v > MyModule.hs, tôi nhận được mô-đun Haskell bắt đầu bằng module Main where.

Có tùy chọn để đặt tên mô-đun Haskell kết quả không?

Tôi hiện đường ống để sed như thế này -

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

nhưng tôi đang tìm kiếm một giải pháp sạch hơn.

Answer 1

Bạn có thể sử dụng Extraction "file" hoặc Extraction Library (hoặc các biến thể của nó), ví dụ:

Definition foo := 6*7. 

Extraction Language Haskell. 
Extraction "MyModule" foo. 

Ở trên tạo ra MyModule.hs tệp, bắt đầu bằng module MyModule where.