[Agda] Announcement: agda2hs release v1.0

[Jason Hu]

That’s great Jesper. But I don’t quite understand the difference between the built-in extraction and agda2hs. I understand that code from agda2hs is more readable, but why can’t we make the built-in extracted code more readable?

Thanks,
Jason Hu

From: Jesper Cockx<mailto:jesper at sikanda.be>
Sent: Friday, April 7, 2023 6:17 AM
To: Agda list<mailto:agda at lists.chalmers.se>
Subject: [Agda] Announcement: agda2hs release v1.0

Dear all,

I am very pleased to announce the first official release of agda2hs, a tool for producing verified and readable Haskell code by extracting it from a (lightly annotated) Agda program. You can find it at https://hackage.haskell.org/package/agda2hs-1.0 or on a cabal package manager near you. The official documentation can be found at https://agda.github.io/agda2hs/, and more details about the motivation and design are available in our paper at the Haskell Symposium: https://dl.acm.org/doi/10.1145/3546189.3549920.

This release is just a first step for agda2hs into the wider world and we have many exciting features that will be added in the future. If you want to report a bug or a feature request, you can do so at https://github.com/agda/agda2hs/issues. We are also open to contributions by new developers, feel free to contact me via email or on Zulip if you have any questions about this.

Best regards,
Jesper Cockx

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230407/f9f202fd/attachment.html>