f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype p a := Pred (Pred a)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder %% should be correct

395efaeb5bf61bc2bf355c1c029dffa09bc1d1edChristian Maedertype

395efaeb5bf61bc2bf355c1c029dffa09bc1d1edChristian Maedertype

f905b9891657dd3eb454d98df87bb0d0cc3796d6Christian Maedertype m b := 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'