agda2hs: Compiling Agda code to readable Haskell.
Produces verified and readable Haskell code by extracting it from a
(lightly annotated) Agda program.
The tool is implemented as an Agda backend, which means that agda2hs
is a
fully functional Agda compiler.
Downloads
- agda2hs-1.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
Versions [RSS] | 1.0, 1.1, 1.2, 1.3 |
---|---|
Dependencies | Agda (>=2.6.3 && <2.6.4), base (>=4.10 && <4.18), containers (>=0.6 && <0.7), deepseq (>=1.4.1.1), directory (>=1.2.6.2 && <1.4), filepath (>=1.4.1.0 && <1.5), haskell-src-exts (>=1.23 && <1.25), mtl (>=2.2), syb (>=0.7), text (>=1.2.3.0), unordered-containers (>=0.2) [details] |
License | BSD-3-Clause |
Copyright | 2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette |
Author | Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette |
Maintainer | jesper@sikanda.be |
Category | Language, Compiler |
Source repo | head: git clone https://github.com/agda/agda2hs.git |
Uploaded | by jcockx at 2023-04-07T10:07:55Z |
Distributions | |
Executables | agda2hs |
Downloads | 300 total (5 in the last 30 days) |
Rating | 2.0 (votes: 1) [estimated by Bayesian average] |
Your Rating | |
Status | Docs not available [build log] Last success reported on 2023-04-07 [all 1 reports] |