Nils Anders Danielsson
Nils Anders Danielsson
> 3. The generated clauses are not looked at for other purposes that might benefit, like matching in the presence of `@0`. Do you mean that we could accept more...
Some [motivation](https://github.com/agda/agda/issues/4653#issuecomment-1166247300).
I think it is unfortunate that the URLs change if you, for instance, replace ```agda F : Set → Set F A = A ``` with the following code: ```agda...
I also noticed that identifiers coming from `open public` get numbered links.
> I also noticed that identifiers coming from `open public` get numbered links. I guess this comment referred to a previous implementation, which not only generated "symbolic anchors", but also...
> I guess this comment referred to a previous implementation, which not only generated "symbolic anchors", but also used such anchors in links. I have re-enabled use of symbolic anchors...
> I have re-enabled use of symbolic anchors in links (#5970), and numbered links are still used for names coming from opened parametrised modules. This part of this issue has...
Note that, while `--experimental-lossy-unification` is faster in these cases, it could lead to unexpected behaviour if Agda instantiates a meta-variable with a solution that is not definitionally equal to the...
If we keep the new flag, then it should be documented in the manual and in the changelog.
> The file UF-Classifiers-Old.lagda takes infinitely long (more than 24 hours before I give up) to type check in the development version of Agda. It takes 4s in the current...