8a77240a809197c92c0736c431b4b88947a7bac1Christian Maedertype p a := Pred (Pred a)

d9a45a35cd696085be1a038b2cc67bee6819c574cmaeder %% should be correct

8a77240a809197c92c0736c431b4b88947a7bac1Christian Maedertype

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maedertype m b := b

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %%

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maedertype m b := b

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski %% both contradict

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescutypes

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maederm : -Type -> Type;

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskip : +Type -> Type

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowskitypes

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederm : -Type -> Type := \ b : -Type . b;

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maederp : +Type -> Type := \ a : +Type . Pred (Pred a)

0095c7efbddd0ffeed6aaf8ec015346be161d819Till Mossakowski### Hint 2.27-2.32, wrong covariance of 'a'

adea2e45fa61f1097aadc490a0aeaf4831b729ccChristian Maeder### Hint 2.27-2.32, no kind found for 'a'

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski*** Error 2.27-2.32, no kind found for 'Pred a'

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski*** Error 4.6, incompatible kind of: m

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder expected: -Type -> Type

09b431a868c79a92ae7c9bd141565f43f9034144Christian Maeder found: +Type -> Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

df11e5eab86d8247f58e301d8f0a2c6ecf4c9541Till Mossakowski