[Agda] id number in html?

[Nils Anders Danielsson]

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:

   https://github.com/agda/agda/blob/6385f850a185523bb5241a71f5a7614a148f6b53/doc/release-notes/2.5.4.md#html-backend

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.

-- 
/NAD