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
the idea is that since each identifier gets linked to the module it was defined in, you could do some tagsoup on the agda --html output to find all of the modules that are explicitly used
this would break if identifiers in a module are only used through instance search though
2
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Would be really neat if Agda could render those in the HTML actually - like as things you could expand interactively in the browser. 🤔