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

class Type < Type

class Type < Type

class Type < Type

class d < Type

class a < d

class a < a

class a < b

class b < d

class d < d

class d < a

type t : a

class h < a

class h < c

type [__] : a -> b

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

var x : b

var x < t

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

a < (b, d)

b < d

c < Type

d < Type

e < Type

f < Type

g < Type

h < (c, a)

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

? : +Type -> Type

Logical : Type := ? Unit

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

Unit : Type

[__] : a -> b

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

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

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

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

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

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

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

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

t : a

%% Type Variables --------------------------------------------------------

x < t : a %(var_4)%

y : Type %(var_2)%

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

bottom : forall a : Type . a %(fun)%

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

false : Unit %(fun)%

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

true : Unit %(fun)%

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

%% Variables -------------------------------------------------------------

x : y

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

*** Warning 3.7, void universe class declaration 'Type'

*** Warning 4.7, void universe class declaration 'Type'

*** Warning 6.7, void universe class declaration 'Type'

*** Error 8.11, not a class 'a'

*** Warning 8.7, unchanged class 'd'

*** Error 13.7, cyclic class 'a'

*** Hint 15.7, refined class 'a'

*** Hint 16.7, refined class 'b'

*** Error 18.7, cyclic class 'd'

*** Error 19.7, cyclic class 'd'

*** Hint 24.7, refined class 'h'

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

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

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

*** Hint 28.24, not a class 'y'

*** Hint 30.7, not a class 's'

*** Error 30.9, unknown type 's'

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

*** Hint 32.5, rebound type variable 'x'

*** Hint 34.5, rebound type variable 'x'

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