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

class Type < Type

class Type < Type

class Type < Type

class d < Type

class a < Type

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

var x : {_ < t}

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

a < (b, d)

b < (c, d, e)

c < Type

d < Type

e < Type

f < Type

g < Type

h < (a, b, c)

j < {v . v < t}

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

Logical : Type := Unit ->? Unit

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

Unit : Type

[__] : a -> b

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

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

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

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

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

t : a

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

y : Type %(var_2)%

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

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__

: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

bottom : forall a : Type . a_v-1 %(fun)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

false : Unit %(fun)%

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

true : Unit %(fun)%

x : y %(var)%

�__ : ? Unit ->? Unit %(fun)%

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

*** Error, 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'

*** Error, illegal type pattern argument '__'