[Agda] mutual strangeness

[Thorsten Altenkirch]

On 1 Feb 2009, at 04:43, Nils Anders Danielsson wrote:

> A better alternative might be to try to come up with
> new rules for mutually recursive definitions, preferably both flexible
> and easy to understand.

Indeed, and moreover these rules should be justified, ideally by a  
translation into a core type theory with a fixed set of combinators.

Luckily we have just obtained funding for a project to work on  
induction-recursion. Which reminds me that I am looking for a clever  
PhD student to work on this subject.

Cheers,
Thorsten

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.