[Agda] Positivity checker, record vs data

[Ulf Norell]

On Tue, Sep 28, 2010 at 4:29 PM, Florent Balestrieri <fyb at cs.nott.ac.uk>wrote:

> Hi,
> I noticed that the positivity check is more lenient with record than data
> definitions. I'd like to understand why, maybe someone could suggest an
> article where this is explained?
>

More than likely this is an oversight rather than intentional. Can you give
an example where this is the case?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100928/187fd2ed/attachment.html