[Agda] C-c C-c turns issue 64 into a bug

[Samuel Bronson]

On Fri, May 16, 2008 at 9:49 AM, Ulf Norell <ulfn at cs.chalmers.se> wrote:

> The problem, which makes the issue tricky to solve, is that open public
> doesn't just give you a new name for an existing definition, it creates a
> new definition. So technically the name that is being printed is out of
> scope.

[examples snipped]

> So when we see A.f it's not simply a matter of printing B.f instead, we need
> to fold the definition of B.f. The reason for things being like this is that
> A might be a parameterised module and we might instantiate it when opening
> it. In this case B.f will be a more interesting definition. That said,
> actually doing the folding should be possible in many cases.

So there would be cases where this would not be possible? I'm having
trouble thinking of how that would arise...