[Agda] Positivity checker, record vs data

Florent Balestrieri fyb at cs.nott.ac.uk
Tue Sep 28 16:29:51 CEST 2010


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?

All the best
-- Florent


More information about the Agda mailing list