Nils Anders Danielsson

I implemented some more things: * The HTML backend now raises an internal error if a duplicate symbolic anchor is detected. I am not entirely certain that this error will...

> If duplicate symbolic anchors are not generated, then it is safe to use them in links Assuming that the anchors are actually generated, which turned out to not always...

> I am not entirely certain that this error will never get raised, but if it does get raised, then we can investigate the problem. The error is raised for...

The commits have not been merged. Can you answer a related [question](https://github.com/agda/agda/pull/5970#issuecomment-1166489102)?

Related: #4526. Some suggestions from that ticket that weren't implemented: * Add a `.agda-lib` file for the builtin modules. * Only allow a single, fixed name for `.agda-lib` files.

> ~I like the idea of only looking for `dir/dir.agda-lib` instead of `dir/*.agda-lib`.~ Never mind, this would make Agda even less usable with Nix (we wouldn't find `/nix/store/0000000000000-cubical/cubical.agda-lib` for example)....

> However, it seems that for published packages a given name like `standard-library.agda-lib` makes some sense. The point of having a fixed name is to avoid having to check if...

> Is there any way around this for now? I'm trying to use something in interactive mode were my top-level module has unsolved metas but all my modules are safe....

> Err so my solution is to add `.` to the end of this line whenever I want to type-check the README directory: If you add `"-i."` to `agda2-program-args`, then...

> A relevant experiment would be to replace the _list_ by `Data.Sequence` or something similar and see if overall performance increases or decreases. Given the high "constant factors" that I...