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

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder %% should be correct

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maedertype m : +Type -> Type := \ b : +Type . b

38adeef4f032b43c6abf7d8a548aa377b13ed2a3Christian Maeder %% should be correct

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder? : +Type -> Type

d48085f765fca838c1d972d2123601997174583dChristian MaederLogical : Type := ? Unit

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian MaederUnit : Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__*__ : +Type -> +Type -> Type

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->?__ : -Type -> +Type -> Type

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

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder%% Assumptions -----------------------------------------------------------

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederbottom : forall a : Type . a %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maederfalse : Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maedernot__ : ? Unit ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maedertrue : Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder�__ : ? Unit ->? Unit %(fun)%

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'