[Agda] id number in html?

Jason Hu fdhzs2010 at hotmail.com
Tue Jun 7 21:28:59 CEST 2022


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?


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

More information about the Agda mailing list