[Agda] unused bindings

Serge D. Mechveliani mechvel at botik.ru
Fri Oct 12 12:28:29 CEST 2012

Dear Agda developers,
the compiler options like
  "warn of unused bindings", 
  "warn of unused import" (of a module or of some its items)

are proved very helpful in Haskell programming, 
and I expect they will be so in Agda.

"The value  x2  is defined but not used" (say,  in (let ... in ...)),
"The item  IsEquivalence  is imported from the module  Foo  but not 
and such.

Though, I cannot tell about its priority.


More information about the Agda mailing list