[Agda] id number in html?

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


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>


More information about the Agda mailing list