The following definition is accepted:
abstract 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