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

a < (e, g)

b

c

d < a

e

f

g

h = (a, b)

j = {_ < t}

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

[__] :a ->b

a__b :a ->b

t :a

x :(a, {_ < t}, b) %(var)%

y :Type %(var)%

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

x : s %(var)%

: y %(var)%

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

Warning (line 3, column 14) redundant universe class

Error (line 3, column 7) illegal universe class declaration

Error (line 4, column 7) illegal universe class declaration

Error (line 6, column 7) illegal universe class declaration

Warning (line 8, column 11) implicit declaration of superclass 'a'

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

Error (line 10, column 24) undeclared class 'h'

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

Error (line 10, column 12) cyclic class relation via 'd'

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

Error (line 12, column 11) cyclic class relation via 'd'

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

Error (line 15, column 11) cyclic class relation via 'a'

Warning (line 17, column 7) redeclared class 'a'

Error (line 17, column 7) class cannot become an alias class 'a'

Warning (line 18, column 7) redeclared class 'b'

Error (line 18, column 7) class cannot become an alias class 'b'

Warning (line 20, column 7) redeclared class 'd'

Error (line 20, column 7) class cannot become an alias class 'd'

Warning (line 25, column 7) redeclared class 'h'

Error (line 25, column 7) inconsistent redefinition of 'h'

Warning (line 27, column 21) unchecked type 't'

Hint (line 31, column 26) not a class 'y'

Hint (line 33, column 9) not a class 's'

Error (line 33, column 9) undeclared type 's'

Hint (line 31, column 26) type 's' is not unifiable with 'y'

Warning (line 37, column 9) unchecked type 't'

Error (line 39, column 6) wrong arity of 'a__'