[Agda] overlapping _∷_, []

[Orestis Melkonian]

Constructor names can overlap; the right one will be chosen on usage 
depending on the expected type.
Note that other kind of names cannot overlap (e.g. definition names, etc..).

Cheers,
--OM

On 22-12-19 20:05, mechvel at scico.botik.ru wrote:
> People,
>
> how does this occur that Data.List.Relation.Unary.All.Properties
> open-imports
>              _∷_, []
>
> both from Data.List  and from  Data.List.Relation.Unary.All
> ?
> Are these constructor names so special that they are overloaded?
>
> Regards,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda