[Agda] Status of Prop

[Wouter Swierstra]

Dear all,

I noticed that Agda has a separate Prop universe. What's the status of  
Prop exactly?  For example, why does this definition get rejected?:

data LT : Nat -> Nat -> Prop where
    Base : forall {n} -> LT Zero n
    Step : forall {n m} -> LT n m -> LT n (Succ m)

Agda says "Set is not less or equal than Prop" - but I imagine the  
more likely explanation is that Prop is just not implemented properly  
yet...

All the best,

   Wouter


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.