[Agda] Status of Prop

[Andres Loeh]

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

I was mainly thinking about Agda's ability to infer the
one inhabitant of the record type, but not the one element
of the datatype.

Cheers,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
http://www.andres-loeh.de