agda2hs
agda2hs copied to clipboard
agda
Compiling Agda code to readable Haskell
It would be nice if we could make some of the functions that are currently defined in the Prelude (such as `if_then_else_`) user-definable instead, and perhaps even allow multiple Agda...
Currently we are missing support for the following classes: - [ ] Real - [ ] Integral - [ ] Fractional - [ ] Floating - [ ] RealFrac -...
It would be good to have some kind of testing that ensures our implementation of the Haskell prelude is correct. For example, for each function we could compile our implementation...
Currently, agda2hs handles transitive imports by importing the names directly from the module where they were originally defined, ignoring any re-exporting layers in the Agda code. We should instead preserve...
Not being able to use the [rewrite construct](https://agda.readthedocs.io/en/v2.6.4.1/language/with-abstraction.html#with-rewrite) is proving to be extremely annoying. Related: #40, #255.
Wonder if we could support `with` syntax for matching on _views_ specifically. https://arxiv.org/pdf/2301.02194.pdf
@omelkonian mentions it would be useful to be able to use `agda2hs` and MAlonzo together in a single project, letting the programmer choose on a per-declaration basis with which backend...