[Agda] Status of Prop

[James Chapman]

On 5 Sep 2008, at 09:10, Andreas Abel wrote:
> Hi Conor,
>
> is not extensionality for singleton types missing here to make your
> example work?

So it seems. Replacing

data TT : Prop where
   tt : TT

with

record TT : Prop where
   field tt : TT

makes the example work.

James

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.