When I extract/compile Coq to Haskell using Extraction Language Haskell.
in the Coq file and running coqtop -compile mymodule.v > MyModule.hs
, I get a Haskell module which starts with module Main where
.
Is there an option to set the resulting Haskell module name?
I currently pipe to sed like this -
coqtop -compile mymodule.v | sed s/Main/MyModule/ > MyModule.hs
but I'm looking for a cleaner solution.
You can use Extraction "file"
or Extraction Library
(or its variants), e.g.
Definition foo := 6*7.
Extraction Language Haskell.
Extraction "MyModule" foo.
The above produces MyModule.hs
file, which starts with module MyModule where
.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With