[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?
More information about the Agda