Nils Anders Danielsson

The documentation could be more explicit about how whitespace is treated. For instance, what happens if the `executables` file contains the following text? ``` agda = /some path/that/contains spaces #...

Could you fix the problem by using `hooray : {A : Set} → A → Term → TC ⊤` instead of `hooray : PostponedTerm → Term → TC ⊤`? Would...

> Alternatively, we could just set the `-Werror` GHC option in the `cabal.project` file and not introduce a new flag at all? Is the idea that this file should not...

I recently wrote some code where, in anticipation of this change, I used projections instead of patterns. I found this to be rather annoying. Here is one example: * With...

> This produces unsolved constraints, in contrast to the variant with hidden tactic arguments. I think hiding or not should not make such a difference here. I suspect that the...

> Before that Agda had checked, or started checking, several files multiple times: Now I've observed this kind of thing again.

I had already saved a `_build` directory which exhibits problematic behaviour. If you download [`issue5245.tgz`](http://www.cse.chalmers.se/~nad/issue5245.tgz) (which I might remove soon), unpack the files, go into the directory `issue5245` and run...

I think that the type error is due to a recent change to Agda, and that I used an older version of Agda when I got the `Failed to validate...

> In any case, the issue seems related to changing options via `.agda-lib` files. Is this something you did around the time the issue occurred, @nad? Yes, I think so.

``` mkdir fresh cd fresh git clone https://github.com/agda/agda-stdlib (cd agda-stdlib && git checkout v1.7.2) git clone https://github.com/graded-type-theory/graded-type-theory cd graded-type-theory git checkout 8858200068f2c42708bfa9f9879a199fbed99ff0 printf '../agda-stdlib/standard-library.agda-lib\ngraded-type-theory.agda-lib' > libraries sed -ri 's/--without-K/--cubical-compatible/' graded-type-theory.agda-lib...