[Agda] Positivity checker

[Nils Anders Danielsson]

On 2008-12-09 11:56, Peter Dybjer wrote:
> 
> It depends on what the termination checker would do when pattern 
> matching on this data type. But my feeling is that there is no natural 
> induction principle associated with this type, except induction on n.

I agree.

> For the case in question (with negative occrurences) I would want
> stronger arguments before it feels worth-while trying to extend the
> positivity checker with some general principle which would instantiate
> to this one.

In practice types like the ones we have been discussing don't seem to
show up that often, so I don't think we should change Agda to support
them. I just speculated about how we /could/ support them, assuming that
we wanted to.

-- 
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.