var s : Type; t : Type

class b < {x . x < s}

%% assume s < t

class a < {x . x < t}

class a < b

class a < {y . y < t}

%% ok (but only for simple tokens)

class a < {y . y < s}

class c, d < Type

class a < (c, d)

class e < a

%% ok

class h < e

%% ok

class h < (a, b)

%% ok

class e < {x . x < t}

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

a < (c, d, {y . y < s}, b, {x . x < t})

b < {x . x < s}

c < Type

d < Type

e < ({x . x < t}, a)

h < (a, b, e)

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

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

Unit : Type := Unit

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

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

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

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

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

s : Type %(var)%

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

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

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

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

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

Hint (line 1, column 5) is type variable 's'

Hint (line 1, column 7) is type variable 't'

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

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

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

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

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

Warning (line 23, column 7) redeclared class 'e'