[Agda] unused values
Sergei Meshveliani
mechvel at botik.ru
Thu Sep 17 15:49:46 CEST 2015
Dear Agda developers,
I point to another reason of why
reporting of unused values and unused import
will be helpful.
When reducing a large program example for the purpose of debugging,
pieces of the code are being commented out. Each comment-out makes some
values and some import unused. Automating the search of these newly
unused things will reduce greatly the process of the example reduction.
For example, currently I have a certain code to reduce for a report.
It needed 6 Gb to type-check. I have spent 8 hours of a stupid work to
reduce this space to 4 Gb, and need to reduce this to 1 Gb. And I do
not reduce unused values, so far, because it takes an effort to find
them.
Regards,
------
Sergei
More information about the Agda
mailing list