[Agda] Status of Prop

[Nils Anders Danielsson]

On Fri, Sep 5, 2008 at 09:46, Andres Loeh <andres at cs.uu.nl> wrote:
>
> Why exactly are these treated differently? I know they
> are, but is the reason for this just an implementation
> detail, or is there a theoretical reason?

I think the reason is mostly practical. Selector functions are not
automatically defined for one-constructor data types, and the selector
functions are needed for η. Furthermore one cannot (currently) pattern
match on records, and it is often nice to be able to pattern match on
things, so one-constructor data types are still useful.

-- 
/NAD