4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass a < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass b < a

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% cycle

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass c < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass d < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass e < c

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% indirect cycle

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass h < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% no implicit declaration

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass g < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass g < (a, b)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% g is already real class

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass i < (g, a)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass g < (a, i)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% cycle via i = g

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass i < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% i is already alias class

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass i < (a, g)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder %% ok

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass i < b

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertype t

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederclass i < {x . x < t}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% Classes ---------------------------------------------------------------

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedera < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederb < a

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederc < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederd < Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedere < c

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederg < (a, b)

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederh < Type

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

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% Type Constructors -----------------------------------------------------

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLogical : Type := Unit ->? Unit

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederUnit : Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__*__ : +Type -> +Type -> Type

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

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__->__ : -Type -> +Type -> Type < __->?__

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__->?__ : -Type -> +Type -> Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedert : Type

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder%% Assumptions -----------------------------------------------------------

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

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

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

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

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

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

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder__when__else__

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

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

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

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederfalse : Unit %(fun)%

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedernot__ : ? Unit ->? Unit %(fun)%

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedertrue : Unit %(fun)%

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

%% Diagnostics -----------------------------------------------------------

*** Error 1.13, not a class 'b'

*** Error 3.11, not a class 'd'

*** Error 4.11, not a class 'e'

*** Error 6.11, not a class 'g'

*** Warning 8.7, redeclared class 'g'

*** Warning 10.7, redeclared class 'g'

*** Error 10.7, cyclic class 'g'

*** Warning 11.7, redeclared class 'i'

*** Warning 12.7, redeclared class 'i'

*** Warning 13.7, redeclared class 'i'

*** Warning 15.7, redeclared class 'i'