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)%

Warning (3,14) redundant universe class

Error (3,7) illegal universe class declaration

Error (4,7) illegal universe class declaration

Error (6,7) illegal universe class declaration

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

Warning (8,7) redeclared class 'd'

Error (10,24) undeclared class 'h'

Warning (10,7) redeclared class 'a'

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

Warning (12,7) redeclared class 'a'

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

Warning (15,7) redeclared class 'a'

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

Warning (17,7) redeclared class 'a'

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

Warning (18,7) redeclared class 'b'

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

Warning (20,7) redeclared class 'd'

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

Warning (25,7) redeclared class 'h'

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

Warning (27,21) unchecked type 't'

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

Error (33,9) undeclared type 's'

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

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

Warning (37,9) unchecked type 't'

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