class Type < Type

var t : Type

class TYPE < {x . x < t}

type : Type- -> Type; Unit : TYPE

class a, b, c < Type

class a, b, c < Type; a < b

type s : c

predfun tt : s ->? Unit

var x : s

program tt : s ->? Unit = \ x : s . ()

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

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

predfun eq : s � s ->? Unit

type s < ? s

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

program And (x, 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

. %(..)%

(fun __=__ : 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) ?

. (fun true : Unit)

forall x : s

forall x : s

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

TYPE < {x . x < t}

a < b

b < Type

c < Type

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

Data1 : Type %[type __ ::=

a : -> __

b : -> __

c : -> __]%

Data2 : Type %[type __ ::=

Cons21 : Data1 �

Data2 -> __ (%(Data2.Cons21.sel_[1,1])% :? Data1)(%(Data2.Cons21.sel_[2,1])% :? Data2)

Cons22 : Data2 �

Data1 -> __ (%(Data2.Cons22.sel_[1,1])% :? Data2)(%(Data2.Cons22.sel_[2,1])% :? Data1)]%

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 := \ a : Type . a ->? Unit

Unit : TYPE := Unit

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

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

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

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

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

s : c < ? s

t : Type %(var)%

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

%(Data2.Cons21.sel_[1,1])% : Data2 ->? Data1 %(select from Data2 constructed by

Cons21 : Data1 � Data2 -> Data2)%

%(Data2.Cons21.sel_[2,1])% : Data2 ->? Data2 %(select from Data2 constructed by

Cons21 : Data1 � Data2 -> Data2)%

%(Data2.Cons22.sel_[1,1])% : Data2 ->? Data2 %(select from Data2 constructed by

Cons22 : Data2 � Data1 -> Data2)%

%(Data2.Cons22.sel_[2,1])% : Data2 ->? Data1 %(select from Data2 constructed by

Cons22 : Data2 � Data1 -> Data2)%

Cons21 : Data1 � Data2 -> Data2 %(construct Data2)%

Cons22 : Data2 � Data1 -> Data2 %(construct Data2)%

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

a : Data1 %(construct Data1)%

: ? s %(Op)%

b : Data1 %(construct Data1)%

c : Data1 %(construct Data1)%

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

eq : s � s ->? Unit %(Pred)%

false : Unit %(Fun)%

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

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

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

true : Unit %(Fun)%

tt : s ->? Unit %(Op)% = \ x : s . ()

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

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

(var y : t)) %()%

(fun true : Unit) %()%

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

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

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

FatalError (line 7, column 11) illegal type pattern argument: __

Error (line 11, column 16) undeclared class '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 20, column 12) unexpected mixfix token: res

Error (line 20, column 10) unexpected pattern '__ res __ (x : s, y : t)'

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

Error (line 21, column 1) no match for 'fst'

Error (line 21, column 1) no type match for 'fst (x : s, y : t)'

Error (line 21, column 1) no typing for 'fst(x : s, y : t) : s'

Error (line 22, column 1) no match for 'snd'

Error (line 22, column 1) no type match for 'snd (x : s, y : t)'

Error (line 22, column 1) no typing for 'snd(x : s, y : t) : t'

Error (line 28, column 9) no match for 'all'

Error (line 28, column 9) no type match for 'all (p : ? s)'

Error (line 28, column 9) no typing for 'all(p : ? s) : ? Unit'

Error (line 30, column 9) no match for 'And'

Error (line 30, column 9) no type match for 'And (x : _var_7, y : ? Unit)'

Error (line 30, column 9) no typing for 'And(x : _var_7, y : ? Unit) : ? Unit'

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

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

Error (line 34, column 10) unexpected pattern '__ or __ (x, y : (? Unit))'

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

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

Error (line 37, column 3) no match for 'ex'

Error (line 37, column 3) no type match for 'ex (p : ? s)'

Error (line 37, column 3) no typing for 'ex(p : ? s) : ? Unit'

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

Error (line 40, column 3) unexpected pattern 'ff ()'

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

Warning (line 61, column 73) data subtype ignored

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

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