ContraVariance.hascasl.output revision bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maedertype m : -Type -> -Type := \ b : -Type . b_v-1
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder %% should be wrong
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder%% Type Constructors -----------------------------------------------------
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian MaederLogical : Type := Unit ->? Unit
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__*__ : +Type -> +Type -> Type
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : -Type -> +Type -> Type < __->?__
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->?__ : -Type -> +Type -> Type
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maederm : -Type -> -Type := \ b : -Type . b_v-1
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 -----------------------------------------------------------
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder*** Error 1.38, incompatible kind of: a
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder expected: -Type
f4d2adb22998bc523bfecc5295460d8b9fa6ea16Christian Maeder*** Error 2.32, incompatible kind of: a
bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder expected: -Type