class Type

var t : Type

class TYPE = Type; TYPE = Type

type Pred : Type- -> Type; Unit : TYPE

class a, b, c

class a, b, c < d; a

type s : c

op tt : s ->? Unit

var x : s

program tt = \ x : s . ()

program __ res __ (x : s, y : t) : s : s = x;

fst(x : s, y : t) : s = (var x : s);

snd(x : s, y : t) : t = (var y : t)

op eq : s � s ->? Unit

type s < ? s

program all(p : ? s) : ? Unit = eq (p, tt)

program And(x : _var_7, y : ? Unit) : ? Unit = t1 () res t2 ()

program __ impl __ (x, y : (? Unit)) = eq (x, x And y)

program __ or __ (x, y : (? Unit)) : ? Unit : ? Unit =

all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);

ex(p : ? s) : ? Unit =

all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);

ff () : ? Unit : ? Unit = all (\ r : (? Unit) . r ())

forall x : t; y : t

. %(..)%

(op __=__ : forall a : Type . a � a ->? Unit) ((var x : t),

(var y : t))

type s

op a : ? s

type Data1 ::= a |

b |

c

type Data2 ::= Cons21 (Data1; Data2) |

Cons22 (Data2; Data1) |

type Data1

type Data3 ::= Cons31 (sel1:? Data1; sel2:? Data2) |

Cons32 (sel2:? Data2; sel1:? Data1)

type Data4 ::= Cons41 (sel1:? Data1; sel2:? Data2) ? |

Cons42 (sel2:? Data2; sel1:? Data1) ?

forall x : s

forall x : s

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

TYPE = Type

a < d

b < d

c < d

d

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

Data1 : Type %[type __ ::=

a : -> __

b : -> __

c : -> __]%

Data2 : Type %[type __ ::=]%

Data3 : Type %[type __ ::=

Cons31 : Data1 � Data2 -> __ (sel1 :? Data1)(sel2 :? Data2)

Cons32 : Data2 � Data1 -> __ (sel2 :? Data2)(sel1 :? Data1)]%

Data4 : Type %[type __ ::=

Cons41 : Data1 � Data2 ->? __ (sel1 :? Data1)(sel2 :? Data2)

Cons42 : Data2 � Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1)]%

Pred : (Type -> Type, Type- -> Type) := \ a : Type . a ->? Unit

Unit : (Type, TYPE) := Unit

s : (c, Type) < ? s

t : Type %(var)%

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

Cons31 : Data1 � Data2 -> Data3 %(construct Data3)%

Cons32 : Data2 � Data1 -> Data3 %(construct Data3)%

Cons41 : Data1 � Data2 ->? Data4 %(construct Data4)%

Cons42 : Data2 � Data1 ->? Data4 %(construct Data4)%

__/\__ : 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

a : Data1 %(construct Data1)%

: ? s

b : Data1 %(construct Data1)%

c : Data1 %(construct Data1)%

def__ : forall a : Type . a ->? Unit

eq : s � s ->? Unit

if__then__else__ : forall a : Type . Unit � a � a ->? a

not__ : Unit ->? Unit

sel1 : Data4 ->? Data1 %(select from Data4 constructed by

(Cons41 : Data1 � Data2 ->? Data4,

Cons42 : Data2 � Data1 ->? Data4))%

: Data3 ->? Data1 %(select from Data3 constructed by

(Cons31 : Data1 � Data2 -> Data3,

Cons32 : Data2 � Data1 -> Data3))%

sel2 : Data4 ->? Data2 %(select from Data4 constructed by

(Cons41 : Data1 � Data2 ->? Data4,

Cons42 : Data2 � Data1 ->? Data4))%

: Data3 ->? Data2 %(select from Data3 constructed by

(Cons31 : Data1 � Data2 -> Data3,

Cons32 : Data2 � Data1 -> Data3))%

tt : s ->? Unit

%% Sentences -------------------------------------------------------------

(op __=__ : forall a : Type . a � a ->? Unit) ((var x : t),

(var y : t)) %()%

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

Error (line 1, column 7) illegal universe class declaration 'Type'

Hint (line 3, column 5) is type variable 't'

Warning (line 5, column 20) redeclared class 'TYPE'

Error (line 5, column 20) inconsistent class redefinition of 'TYPE'

Warning (line 11, column 16) implicit declaration of superclass 'd'

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

Warning (line 11, column 10) redeclared class 'b'

Warning (line 11, column 13) redeclared class 'c'

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

Error (line 11, column 19) class cannot become an alias class 'a'

Error (line 20, column 12) unexpected mixfix token: res

Error (line 20, column 37) unexpected mixfix token: x

Hint (line 15, column 11) type 's' is not unifiable with 's ->? Unit'

Error (line 28, column 41) no match for 'tt'

Error (line 28, column 35) no type match for 'eq (p, tt)'

Error (line 28, column 35) no typing for 'eq (p, tt)'

Error (line 30, column 40) unexpected mixfix token: t1

Error (line 32, column 12) unexpected mixfix token: impl

Error (line 34, column 12) unexpected mixfix token: or

Error (line 35, column 19) unexpected mixfix token: x

Error (line 34, column 44) unexpected mixfix token: all

Error (line 38, column 32) unexpected mixfix token: impl

Error (line 38, column 17) unexpected mixfix token: all

Error (line 37, column 27) unexpected mixfix token: all

Error (line 40, column 7) unexpected mixfix token: )

Error (line 40, column 20) unexpected mixfix token: all

Warning (line 57, column 11) redeclared type 's'

Error (line 61, column 36) unknown type 'Data2'

Error (line 61, column 52) unknown type 'Data2'

Warning (line 61, column 73) data subtype ignored

Error (line 66, column 8) unexpected mixfix token: true

Error (line 66, column 25) unexpected mixfix token: e

Error (line 67, column 12) unexpected mixfix token: e