[Agda] Mendori

[Peter G. Hancock]

>>>>> jeff polakow wrote (on Mon, 21 Feb 2005 at 04:45):

    > Hello,
    >   I have just added Mendori, an experimental implementation of a logical
    > framework with dependently typed records, to the CVS repository. The
    > code is still buggy and unstable, but it might be of interest to some of
    > you.

What are dependently typed records?  What do they give you beyond
sig types, and single constructor data types?

Peter Hancock