f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype p : +Type -> Type := \ a : +Type . Pred (Pred a)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder %% should be correct

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedersort

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedersort

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maedertype m : +Type -> Type := \ b : +Type . b

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder %% should be correct

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder%% Type Constructors -----------------------------------------------------

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederm : +Type -> Type := \ b : +Type . b

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederp : +Type -> Type := \ a : +Type . Pred (Pred a)

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder%% Diagnostics -----------------------------------------------------------

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 2.27-2.32, wrong covariance of 'a'

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

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder*** Error 2.27-2.32, no kind found for 'Pred a'

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 3.27, wrong contravariance of 'b'

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder*** Error 3.27, no kind found for 'b'