[Agda] Status of Prop

[Andres Loeh]

> So it seems. Replacing
>
> data TT : Prop where
>   tt : TT
>
> with
>
> record TT : Prop where
>   field tt : TT
>
> makes the example work.

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?

Cheers,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

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