Andreas Abel
Andreas Abel
For documentation and testing of Agda, it would be nice to have `failure` blocks similar to MiniAgda. This could be realized by putting the to-fail definitions in an anonymous module...
GHC 9.4.0.20220523 has been released (GHC 9.4.1 alpha2). This is an umbrella issue to track migration to GHC 9.4.1. It looks like it is mainly the ecosystem we have to...
Add option `--cwd DIR` to change to `DIR` before doing anything else relative to a dir. Motivation: - `cabal run agda` needs to be run from the agda repo root...
Reported by @Saizan. Lifted from: - https://github.com/agda/agda/issues/1023#issuecomment-765223893 ```agda {-# OPTIONS --without-K #-} data Zero : Set where data Id (X : Set) : Set where i : X → Id...
@jespercockx, I was wondering why `PiSort` does not behave like a usual `Def`, meaning that if it cannot compute to a sort value because of unsolved metas, it would signal...
I have been once more searching for dynamic graph libraries today on hackage and didn't find anything suitable... I am playing with the idea of publishing `Agda.Utils.Graph.AdjacencyMap.Unidirectional` as - package...
Currently, when I open a `.agda` file with `C-x C-f` in Emacs, it is just black-and-white, even when an up-to-date `.agdai` file exists. It would be nice if highlighting was...
I'd like generalization to kick in also when in a type signature there is an unsolved meta originating from a generalization. ```agda open import Agda.Builtin.Nat variable n : Nat data...
The usual convention in math is that the shapes of inf/sup-operators are chosen consistent with the shape of the comparison relation, with typical flavors being: - rectangular - round -...
I was expecting that `DecTotalOrder` gives me operations to compute the minimum and maximum, but could not find them. (These are declared in the `Lattice` hierarchy.) I think it would...