[Agda] unused values

[Andrés Sicard-Ramírez]

On 17 September 2015 at 08:49, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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.

I agree.

>
> 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.

Keep in mind that in the past someone else has done this job. I hope
you had realised why is important reporting a bug using a MVE (
https://en.wikipedia.org/wiki/Minimal_Working_Example ).

-- 
Andrés