[Agda] id number in html?

Nils Anders Danielsson nad at cse.gu.se
Wed Jun 8 14:08:58 CEST 2022

On 2022-06-07 21:28, Jason Hu wrote:
> When generating html files, Agda assigns an id to each definitions.
> Now when we need to refer to that id from elsewhere, e.g. another
> website, how stable can I assume this id to be?

The identifiers correspond to file positions.

> Is there a more recommended way to create links to an Agda html file?

The HTML backend also creates (HTML) identifiers based on the names of
(Agda) identifiers:


The current naming scheme is a little buggy
(https://github.com/agda/agda/issues/4653) and might change in the
future. If you use this kind of link, then I suggest that you test that
it points to the right thing.


More information about the Agda mailing list