idea (VERY CURSED): Identify unused Agda imports based on the generated HTML
Conversation
Details? It's kind of intriguing. One of my students has this habit of leaving TONS of unused imports around, and I obsessively clean it all out. Anything that would make that easier, even cursed, would be an improvement.
4
5
Replying to
Dang, do you not get warnings for this kind from Agda? Seems like it'd be a pain to keep on top of. 😢