[Agda] mutual strangeness

[Nils Anders Danielsson]

On 2009-02-01 12:16, Thorsten Altenkirch wrote:
> 
> 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.

Indeed. Moreover this translation should ideally be simple and
transparent, and the core theory simple and consistent. :)

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