The following definition is accepted:


   Id : Set -> Set
   Id x = x

 data X : Set where
   x : Id X -> X

However, if Id is placed in a separate module (separate file), then the definition of X is not accepted by the positivity checker.

Page last modified on October 16, 2007, at 12:32 PM
Powered by PmWiki