[Agda] id number in html?

[Jason Hu]

Hi,

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? Is there a more recommended way to create links to an Agda html file?

Thanks,
Jason



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220607/fa851d60/attachment.html>