Nils Anders Danielsson
Nils Anders Danielsson
If you use `opaque` a lot, then you can get quite a bit of noise in the code: * The `opaque` blocks are indented. * There is an `opaque` keyword...
Perhaps it makes sense to support erased import statements: ```agda import @0 M open import @erased N ``` @jespercockx [wrote](https://github.com/agda/agda/issues/4743#issuecomment-1025961462) that "it would be good to be able to add...
The following sequence of commands succeeds if Agda 2.6.4-9afe77020541b944331685ef2720a81bb312a925 is used, but fails with Agda-2.6.4-2af2ff114d167d9931034ca16d1bf6ba04efe661: ``` mkdir fresh && cd fresh (git clone https://github.com/agda/agda-stdlib.git && cd agda-stdlib && git checkout...
The GHC backend calls GHC directly. However, this might not work very well if the code relies on some Haskell package (like `ieee754`). It might make sense to provide some...
In the following code the warning `NotAffectedByOpaque` is turned off, and Agda does not print any warning, but the definition of `R` is still highlighted with `agda2-highlight-deadcode-face`: ```agda {-# OPTIONS...
Uses of `@tick`/`@lock` that are ignored should trigger warnings or errors. For instance, I suspect that the following uses of `@lock` are ignored: ```agda postulate @lock _ : Set @lock...