Jesper Cockx
Jesper Cockx
In https://github.com/agda/agda/issues/6049#issuecomment-1293718186, @martinescardo noted that he would like to have a flag to turn off irrelevance, and I agree that it would be nice to have such a flag (and...
Minimal example: ```agda data D : Set {-# COMPILE AGDA2HS D #-} data D where C : D ``` This generates an empty Haskell file. It should either raise an...
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...
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...
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...
Currently we only support fixed universes `Set`, `Set1`, `Set2`, to cover more of Agda we should expand this to include universe-polymorphic functions.
We eventually want to check that functions are terminating, but ideally without adding a whole termination checker to the trusted code base. Instead, we could have a set of judgements...
Currently we do not check positivity in any way, we should actually check that the datatypes we define are strictly positive (see also https://github.com/jespercockx/agda-core/issues/29). However, we should be careful to...
Currently the typing rule for `let`-bindings is rather weak, because the typing of the body cannot make use of the value of the `let`-bound variable. To make the typing of...
Our evaluator is already set up with the possibility of lazy evaluation, all we'd need to do is the following: - [ ] Keep track of which values in the...