[Agda] unclear import report

Nils Anders Danielsson nad at chalmers.se
Fri Mar 15 16:00:18 CET 2013


On 2013-03-13 12:53, Serge D. Mechveliani wrote:
> 1. The report does not show where the import diverges.
>     The user needs to search through a lengthy code in a hope to find a
>     pair of responsible places.
> Can this report be fixed in Agda ?

Perhaps one could give some sort of "stack trace", showing the locations
of the various module operations. If you have a concrete suggestion,
please document it in a feature request on the bug tracker.

> 2. After I have found the place, I fix the error by inserting
>     " using () "  after  "open Monoid subMon".
> I thought that
>                 open Monoid subMon renaming (invMb to invMb-sub)
>
> means to open only  invMb -- with renaming.
> But, probably, it also opens all other items. Does it?

Yes.

-- 
/NAD


More information about the Agda mailing list