[Agda] id number in html?

Nils Anders Danielsson nad at cse.gu.se
Wed Jun 8 20:46:02 CEST 2022


On 2022-06-08 15:34, Jason Hu wrote:
> If I read your answer correctly, even comments will shift the id
> number?

Yes. Note that even comments get identifiers, so you can link to a
comment.

> Wouldn’t that be a bit fragile?

Yes.

> At this point, is there a way to use a different id scheme?

Yes, the other scheme that I mentioned.

-- 
/NAD


More information about the Agda mailing list