[Agda] Status of Prop

[Ulf Norell]

On Mon, Sep 1, 2008 at 10:10 AM, Wouter Swierstra <wss at cs.nott.ac.uk> wrote:

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


Prop is experimental at the moment. The rules are

Prop < Set
Prop : Set1

A : Set   P : Prop
-----------------------
(x : A) -> P : Prop

Your datatype is rejected since the natural number arguments to the
constructors won't
fit in Prop (Set is not less or equal than Prop).

There's a flag --proof-irrelevance which makes Prop proof irrelevant, but
also ensures that
propositions have at most one element by restricting datatypes in Prop to
have at most one
constructor.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080902/5d0f344b/attachment.html