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 -> b

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

var

var x : b

var x : {_ < t}

type : 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

t : a

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

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

__if__ : Unit � Unit ->? Unit %(Fun)%

__when__else__ : forall a : Type . a � Unit � a ->? a %(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)%

x : y %(var)%

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

*** Error 3.7, illegal universe class declaration 'Type'

*** Error 4.7, illegal universe class declaration 'Type'

*** Error 6.7, illegal universe class declaration 'Type'

*** Error 8.11, undeclared class 'a'

*** Warning 8.7, redeclared class 'd'

*** Error 10.24, undeclared class 'h'

*** Warning 12.7, redeclared class 'a'

*** Warning 15.7, redeclared class 'a'

*** Error 15.7, cyclic class 'a'

*** Warning 17.7, redeclared class 'a'

*** Warning 18.7, redeclared class 'b'

*** Warning 20.7, redeclared class 'd'

*** Error 20.7, cyclic class 'd'

*** Warning 25.7, redeclared class 'h'

*** FatalError 29.7, illegal type pattern argument: __

*** Hint 31.5, is type variable 'x'

*** Hint 31.12, is type variable 'y'

*** Error 33.9, unknown type 's'

*** Hint 35.5, is type variable 'x'

*** FatalError 39.8, illegal type pattern argument: __