[Agda] Difference between two datatypes

[Sean Leather]

Hi,

Sorry for so many questions, but here's another.

What are the differences (if any) between the following two datatypes?

data X (a : Set) : Set where
  x : a -> X a

data Y : Set -> Set1 where
  y : {a : Set} -> a -> Y a

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080619/271e1565/attachment-0001.html