class a < Type

class b < a

%% cycle

class c < Type

class d < Type

class e < c

%% indirect cycle

class h < Type

%% no implicit declaration

class g < Type

class g < (a, b)

%% g is already real class

class i < (g, a)

class g < (a, i)

%% cycle via i = g

class i < Type

%% i is already alias class

class i < (a, g)

%% ok

class i < b

var t : Type

class i < {x . x < t}

%% Classes ---------------------------------------------------------------

a < Type

b < a

c < Type

d < Type

e < c

g < (a, b)

h < Type

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

%% Type Constructors -----------------------------------------------------

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : Type := Unit

__-->__ : Type- -> Type+ -> Type

__-->?__ : Type- -> Type+ -> Type

__->__ : Type- -> Type+ -> Type

__->?__ : Type- -> Type+ -> Type

__�__ : Type+ -> Type+ -> Type

t : Type %(var)%

%% Assumptions -----------------------------------------------------------

__/\__ : Unit � Unit ->? Unit %(Fun)%

__<=>__ : Unit � Unit ->? Unit %(Fun)%

__=__ : forall a : Type . a � a ->? Unit %(Fun)%

__=>__ : Unit � Unit ->? Unit %(Fun)%

__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

__\/__ : Unit � Unit ->? Unit %(Fun)%

def__ : forall a : Type . a ->? Unit %(Fun)%

false : Unit %(Fun)%

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

not__ : Unit ->? Unit %(Fun)%

true : Unit %(Fun)%

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

Error (line 1, column 13) undeclared class 'b'

Error (line 3, column 11) undeclared class 'd'

Error (line 4, column 11) undeclared class 'e'

Error (line 6, column 11) undeclared class 'g'

Warning (line 8, column 7) redeclared class 'g'

Warning (line 10, column 7) redeclared class 'g'

Error (line 10, column 7) cyclic class 'g'

Warning (line 11, column 7) redeclared class 'i'

Warning (line 12, column 7) redeclared class 'i'

Warning (line 13, column 7) redeclared class 'i'

Hint (line 14, column 5) is type variable 't'

Warning (line 15, column 7) redeclared class 'i'