When extracting from coq to haskell, is it possible to map a coq function to a function from a third party library?
I suppose we would also need a way to import that library in the extracted code. Is there a way to do that?
I thought I saw somewhere that we can't add an
import in the extracted haskell code. But I couldn't find that link now.
Extract Constant command for overriding definitions, but for
import you have to post-process the extracted code yourself.
Julin S has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC