[Agda] Good old times

[Nils Anders Danielsson]

On 2009-02-16 10:45, Pierre Hyvernat wrote:

> What would be possible is to have a minimal logical framework (dependent
> products, dependent records, inductive types, Set and Type). I'm not
> even sure I'd want inductive families in there...
>
> I am thinking, something along the lines of Thierry's first prototypes,
> with: decent error reporting, minimal standard library, small Emacs
> mode.
> It could be done in less than 2000 loc. (Random guess.)

If this is what you want, then I think you should use one of Thierry's
prototypes. I think he has a new version with support for coinduction,
though. :)

> About the dependencies, what concerns me is to see Agda depending on
> such things as "xhtml-3000.2.0.1" and others.  I mean, part of Agda is
> about the foundation of mathematics. It is not just another programming
> language...

I don't think you should worry too much about such dependencies; bugs in
the Agda type checker are more likely to come from code written by us.

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