09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maedertype p : +Type -> Type := \ a : +Type . Pred (Pred a_v-1)@(Pred a_v-1@(a_v-1 ->? Unit) ->? Unit)

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder %% should be correct

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maedertype m : +Type -> Type := \ b : +Type . b_v-1

38adeef4f032b43c6abf7d8a548aa377b13ed2a3Christian Maeder %% should be correct

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian MaederLogical : Type := Unit ->? Unit

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian MaederPred : -Type -> Type := \ a : -Type . a_v-1 ->? 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

14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maederm : +Type -> Type := \ b : +Type . b_v-1

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maederp : +Type -> Type

09c434a9e1590a40f8711547d107ff3a2717eb6dChristian Maeder := \ a : +Type . Pred (Pred a_v-1)@(Pred a_v-1@(a_v-1 ->? Unit) ->? Unit)

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

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

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder__when__else__

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maederbottom : forall a : Type . a_v-1 %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maederfalse : Unit %(fun)%

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

f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maedertrue : Unit %(fun)%

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

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder*** Hint 2.27-2.32, wrong covariance of 'a'

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

ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder*** Hint 3.27, wrong contravariance of 'b'

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