I am looking for code in Coq and extracting this code for use in a large Haskell project. I want to create a single module in Coq, prove properties, and then use the Haskell module system to prevent violations of these properties (via smart constructors).
I can’t find any signs that it is possible to extract Coq code into a Haskell module with an explicit export list. It seems I have to manually modify the extracted Coq code, which is not a big deal, but I want to know if I have this right. Does anyone have an alternative suggestion?
source
share