[Agda] Positivity checker

[Nils Anders Danielsson]

On 2008-12-10 04:36, Gyesik Lee wrote:
>> I find your arguments for prefering inductively to recursively defined
>> families interesting, but hardly conclusive. My own feeling is that it
>> depends on the situation which is better. For cases like Vec, the inductive
>> one is a "generator" and the recursive one simplifies.
> 
> I agree. My experience with Coq tells me it really depends on the
> situation whether you should choose for an inductive definition or for
> a recursive function, of course when you have both options.

Right, sometimes you want things to evaluate more, and then a recursive
definition can be useful.

-- 
/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.