agda2hs
agda2hs copied to clipboard
agda
Compiling Agda code to readable Haskell
I'm using some simple macros to generate parts of my `agda2hs` code. However, I noticed this can lead to terms being generated that refer to unbound variables. Here is a...
See https://github.com/agda/agda2hs/issues/262 cc @jespercockx This is my first PR to agda2hs. I am also new to Agda in general. This draft is a way of showing what I currently have...
If I have a module `AAA` that imports another module `AAABBB`, then this import is dropped from the generated Haskell code. The cause is located here: https://github.com/agda/agda2hs/blob/0fc20ccd031a07c848824fc125839b4d91e35667/src/Agda2Hs/Compile/Imports.hs#L28 (Git blame tells...
The laws for `Eq` are defined by asserting that the `==` decision procedure actually `Reflect`s the type of propositional equality `≡`, while the laws for `Ord` do not use this...
In the Agda standard library, the syntax of `≡˘⟨_⟩` was changed to `≡⟨_⟨`. Maybe it should be changed here as well but I am not sure: https://github.com/agda/agda2hs/blob/fdbebb664feb229514ba5cc0a5f817f80e790219/lib/Haskell/Law/Equality.agda#L59
[See `\cases`](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/lambda_case.html) supported since GHC `9.4.1`.
This fixes #119 by raising a warning when an unknown name appears in the generated Haskell code. The following names are considered as "known": - Names that have a COMPILE...
Following some discussion at Zurihac, I wanted to give my take on the formatting/linting question. This change will impact practically every file in the codebase, which can be difficult for...
As suggested by @HeinrichApfelmus in https://github.com/agda/agda2hs/issues/366#issuecomment-2377083047 and https://github.com/agda/agda2hs/issues/366#issuecomment-2377411491
It seems like we're long overdue for a new release (as indicated by the comment by @HeinrichApfelmus in https://github.com/agda/agda2hs/issues/361#issuecomment-2364047031_). One thing that might be worth doing is to investigate some...