[Agda] id number in html?
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...
More information about the Agda