var s : Type; t : Type

class b={x.x< s}

%% assume s < t

class a={x.x< t}

class a < b

%% a is an alias class

class a={y.y< t}

%% ok (but only for simple tokens)

class a={y.y< t}

%% wrong redefinition

class c, d

class a = {_ < t}

%% wrong redefinition

class e = a

%% ok intersection

class h < e

%% ok

class h < (a, b)

%% ok

class e = a

%% wrong because e is intersection class

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

a = {_ < t}

b = {_ < s}

c

d

e = a

h < (a, b, e)

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

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

Unit : Type := Unit

s : Type %(var)%

t : Type %(var)%

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

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'

Error (line 7, column 7) alias class cannot become a real class 'a'

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

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

Error (line 11, column 7) inconsistent downset of 'a'

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

Error (line 15, column 7) inconsistent class redefinition of 'a'

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

Warning (line 21, column 12) already known as super class 'a'

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

Error (line 23, column 7) inconsistent class redefinition of 'e'