Julin S (Jul 19 2022 at 06:29): Julin S (Jul 19 2022 at 06:29):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?
Julin S (Jul 19 2022 at 06:29):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.
Li-yao (Jul 19 2022 at 07:50):There's an Extract Constant command for overriding definitions, but for import you have to post-process the extracted code yourself.
Julin S (Jul 20 2022 at 05:21):Thanks!
Notification Bot (Jul 20 2022 at 05:21):Julin S has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC