PlainTypes.hascasl.output revision c1124c6303c288db3fcb40518d38169cd7baaa4c
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederclass a, b, c, d < Type
81d182b21020b815887e9057959228546cf61b6bChristian Maedertype [__], {__} : a -> b
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maedervar u : [r]; v : {s}
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maedertype tuple3 : a -> b -> c -> d
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedervar x : tuple3 r s t
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedertype tuple1 : b -> a
fbb66ee3e170624835b99f7aa91980753cb5b472Christian Maedertype m : (a -> b) -> c
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedertype List : a -> b
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedervar v : m List
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedervar nt : a -> (b -> c) -> c -> d
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedertype s1, r1, t1 < t
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedertype s2 = r2 = t2
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maedertype s3 : Type := t
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder%% Classes ---------------------------------------------------------------
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder%% Type Constructors -----------------------------------------------------
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederPred : Type -> Type := \ a : Type . a ->? Unit
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederUnit : Type := Unit
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder__-->__ : Type- -> Type+ -> Type
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maeder__-->?__ : Type- -> Type+ -> Type
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__->__ : Type- -> Type+ -> Type
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder__->?__ : Type- -> Type+ -> Type
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder__�__ : Type+ -> Type+ -> Type
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederm : (a -> b) -> c
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maedernt : a -> (b -> c) -> c -> d %(var)%
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederr2 : Type < (t2, r2, s2)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskis2 : Type < (t2, r2, s2)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeders3 : Type := t
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedert2 : Type < (t2, r2, s2)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskituple1 : b -> a
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maedertuple3 : a -> b -> c -> d
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder%% Assumptions -----------------------------------------------------------
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder__/\__ : Unit � Unit ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__<=>__ : Unit � Unit ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__=__ : forall a : Type . a � a ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__=>__ : Unit � Unit ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder__\/__ : Unit � Unit ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__if__ : Unit � Unit ->? Unit %(Fun)%
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maederdef__ : forall a : Type . a ->? Unit %(Fun)%
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederfalse : Unit %(Fun)%
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederif__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedernot__ : Unit ->? Unit %(Fun)%
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maedertrue : Unit %(Fun)%
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederu : [r] %(var)%
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederv : m List %(var)%
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder : {s} %(var)%
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maederx : tuple3 r s t %(var)%
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder%% Diagnostics -----------------------------------------------------------
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder*** Error 12.9, incompatible kind of: tuple3 r s
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder expected: Type
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder found: c -> d
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder*** Error 18.12, unexpected place '__'
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder*** Error 24.10, incompatible kind of: m
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder expected: Type
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder found: (a -> b) -> c
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder*** Error 26.12, incompatible kind of: tuple1
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder expected: a -> b
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder found: b -> a
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder*** Error 28.12, incompatible kind of: tuple3
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder expected: a -> b
3c62e6ef442caf092adcbecf6fccd957dcd72689Christian Maeder found: a -> b -> c -> d
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder*** Hint 30.5, is type variable 'nt'
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder*** Error 32.15, incompatible kind of: List
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder expected: b -> c
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder found: a -> b
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder*** Error 38.19, ambiguous typings
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder '(fun __=__ : forall a : Type . a � a ->? Unit) ((var x : t),
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder (var x : t))' (38.19)
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder '(fun __=__ : forall a : Type . a �
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder a ->? Unit) ((var x : tuple3 r s t), (var x : tuple3 r s t))' (38.19)