01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass a < Type

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass b < a

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski %% cycle

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiclass c < Type

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederclass d < Type

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass e < c

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder %% indirect cycle

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass h < Type

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder %% no implicit declaration

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederclass g < Type

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiclass g < (a, b)

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski %% g is already real class

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass i < (g, a)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederclass g < (a, i)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder %% cycle via i = g

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederclass i < Type

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder %% i is already alias class

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederclass i < (a, g)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder %% ok

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederclass i < b

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskivar t : Type

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangclass i < {x . x < t}

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder%% Classes ---------------------------------------------------------------

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maedera < Type

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederb < a

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederc < Type

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangd < Type

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maedere < c

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maederg < (a, b)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederh < Type

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederi < ({x . x < t}, b, a, g)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder%% Type Constructors -----------------------------------------------------

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiPred : Type -> Type := \ a : Type . a ->? Unit

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederUnit : Type := Unit

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder__*__ : Type+ -> Type+ -> Type

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder__-->__ : Type- -> Type+ -> Type

90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder__-->?__ : Type- -> Type+ -> Type

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder__->__ : Type- -> Type+ -> Type

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich__->?__ : Type- -> Type+ -> Type

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luetticht : Type %(var)%

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich%% Assumptions -----------------------------------------------------------

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich__/\__ : Unit * Unit ->? Unit %(fun)%

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

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

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski__=>__ : Unit * Unit ->? Unit %(fun)%

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

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

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder__if__ : Unit * Unit ->? Unit %(fun)%

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu__when__else__ : forall a : Type . a * Unit * a ->? a %(fun)%

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maederbottom : forall a : Type . a %(fun)%

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maederfalse : Unit %(fun)%

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedernot__ : Unit ->? Unit %(fun)%

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maedertrue : Unit %(fun)%

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder%% Diagnostics -----------------------------------------------------------

8e80792f474d154ff11762fac081a422e34f1accChristian Maeder*** Error 1.13, undeclared class 'b'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Error 3.11, undeclared class 'd'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Error 4.11, undeclared class 'e'

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder*** Error 6.11, undeclared class 'g'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Warning 8.7, redeclared class 'g'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Warning 10.7, redeclared class 'g'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Error 10.7, cyclic class 'g'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder*** Warning 11.7, redeclared class 'i'

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder*** Warning 12.7, redeclared class 'i'

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder*** Warning 13.7, redeclared class 'i'

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder*** Hint 14.5, is type variable 't'

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder*** Warning 15.7, redeclared class 'i'

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder