[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
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