[Agda] Mapping QNames to module names?

Alan Jeffrey ajeffrey at bell-labs.com
Tue Oct 4 15:43:40 CEST 2011


Do I not have to worry about the case where there's top level modules 
Foo and Foo.Bar when emitting Foo.Bar.baz?

On 10/04/2011 01:12 AM, Ulf Norell wrote:
>
> On Mon, Oct 3, 2011 at 9:33 PM, Alan Jeffrey <ajeffrey at bell-labs.com
> <mailto:ajeffrey at bell-labs.com>> wrote:
>
>     Ah good point, finding the longest top-level visited module name
>     which is a prefix of the qname should do the trick.
>
>
> Actually, there can be only one. Different top-level modules have
> different IDs even if the string names are the same.
>
> / Ulf


More information about the Agda mailing list