Stream: Coq users

Topic: ✔ Extracting function to 3rd party function


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Jul 20 2022 at 05:21):

Thanks!

view this post on Zulip Notification Bot (Jul 20 2022 at 05:21):

Julin S has marked this topic as resolved.


Last updated: Jun 18 2024 at 22:01 UTC