class b, c, d, e, f, g < Type

class Type < Type

class Type < Type

class Type < Type

class d < Type

class a < (d, e, g)

class a < d

class a < a

class a < b

class b < (c, d, e)

class d < d

type t : a

class h < (a, b)

class h < c

class j < {v . v < t}

type a, [ : a -> b

var x : a; y : Type; x : y

var

var x : b

var x : {_ < t}

type a : b

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

a < (b, d, e, g)

b < (c, d, e)

c < Type

d < Type

e < Type

f < Type

g < Type

h < (c, a, b)

j < {v . v < t}

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

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

Unit : Type := Unit

[ : a -> b

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

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

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

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

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

a : a -> b

t : a

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

y : Type %(var)%

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

__/\__ : Unit � Unit ->? Unit

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

def__ : forall a : Type . a ->? Unit

if__then__else__ : forall a : Type . Unit � a � a ->? a

not__ : Unit ->? Unit

x : y %(var)%

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

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

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

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

Error (line 8, column 11) undeclared class 'a'

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

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

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

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

Error (line 15, column 7) cyclic class 'a'

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

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

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

Error (line 20, column 7) cyclic class 'd'

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

Hint (line 31, column 5) is type variable 'x'

Hint (line 31, column 12) is type variable 'y'

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

Hint (line 35, column 5) is type variable 'x'

Error (line 39, column 6) incompatible kind of: a

expected: Type -> Type

found: Type