[Agda] overlapping _∷_, []

mechvel at scico.botik.ru mechvel at scico.botik.ru
Sun Dec 22 21:05:17 CET 2019

Previous message (by thread): [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1
Next message (by thread): [Agda] overlapping _∷_, []
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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

Previous message (by thread): [Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1
Next message (by thread): [Agda] overlapping _∷_, []
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the Agda mailing list