%% all warnings

class a < b

%% implicit super class declaration

class b

%% redeclared class

class c < Type

%% useless (always true)

class d < a

%% ok

class d < b

%% transitive via a

class d < a

%% direct repetition

class e < f

%% Type is silently ignored

class g < h

%% doubles are silently ignored

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

a < b

b

c

d < (a, b)

e < f

f

g < h

h

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

Unit : Type

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

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

Warning (line 2, column 11) implicit declaration of superclass 'b'

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

Warning (line 4, column 11) redundant universe class

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

Warning (line 6, column 11) already known as super class 'b'

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

Warning (line 7, column 11) already known as super class 'a'

Warning (line 8, column 18) implicit declaration of superclass 'f'

Warning (line 9, column 12) implicit declaration of superclass 'h'