Andreas Abel
Andreas Abel
https://github.com/BNFC/bnfc/blob/c2897d032338b541a5a54793d805993d49e0f79c/source/src/BNFC/Backend/Haskell/CFtoAlex3.hs#L65
Java's `enum`, `record`, and `sealed interface` could be utilized for a compact representation of the abstract syntax, residing in a single module rather than a package. It follows a grammar...
@jespercockx: I am trying to understand confluence because of the open PR #7934. - #7934 The explanation at the top of the module `Confluence` feels odd: https://github.com/agda/agda/blob/c255c8091f09882a3c4e1a1ec3db6dbee91f0e84/src/full/Agda/TypeChecking/Rewriting/Confluence.hs#L24-L26 Why do we...
It seems like with `--build-library`, rewrite rules from a previous loaded module are active when building the next module, which is definitely unsound. To reproduce, make two modules `Nat1` and...
Since the imported signature contains all rewrite rules we visited during loading various modules (see #4272), we need to filter out those that are currently not (transitively) imported. To this...
The [user manual](https://agda.readthedocs.io/en/v2.8.0-rc3/language/rewriting.html) currently does not document how rewrite rules interact with the module system and imports. I also do not know what the intended behavior is, do you, Jesper...
- **Bump version to 2.7.20250510**. (2.8.0-rc1) - **Agda.cabal: replace -Werror by -Wwarn** - **Agda.cabal: remove test-suite**
- **Bump version to 2.7.20250510** - **Agda.cabal: replace -Werror by -Wwarn** - **Agda.cabal: remove test-suite** Candidate: https://hackage.haskell.org/package/Agda-2.7.20250510/candidate Candidate 2: https://hackage.haskell.org/package/Agda-2.7.20250524/candidate Candidate 3: https://hackage.haskell.org/package/Agda-2.7.20250601/candidate
```agda record R : Set₂ where field f : Set₁ v : R v = record where f = Set r1 : R r1 = record where open R v...
```agda record R : Set₁ where field f : Set r : R r = record where postulate f : Set ``` This gives yellow and an unsolved meta. What...