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

__if__ : Unit � Unit ->? Unit %(Fun)%

__when__else__ : forall a : Type . a � Unit � a ->? a %(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 1.7, illegal universe class declaration 'Type'

*** Hint 3.5, is type variable 't'

*** FatalError 7.11, illegal type pattern argument: __

*** Error 11.16, undeclared class 'd'

*** Warning 11.7, redeclared class 'a'

*** Warning 11.10, redeclared class 'b'

*** Warning 11.13, redeclared class 'c'

*** Warning 11.19, redeclared class 'a'

*** Error 20.12, unexpected mixfix token: res

*** Error 20.10, unexpected pattern '__ res __ (x : s, y : t)'

*** Error 20.37, unexpected mixfix token: x

*** Hint 21.1, no type match for: fst

with type: '_var_4 ->? s' (line 21, column 20)

known types:

*** Hint 21.1, wrong result type 's' (line 21, column 20)

for application 'fst (x : s, y : t)'

*** Error 21.1, no typing for 'fst(x : s, y : t) : s'

*** Hint 22.1, no type match for: snd

with type: '_var_5 ->? t' (line 22, column 20)

known types:

*** Hint 22.1, wrong result type 't' (line 22, column 20)

for application 'snd (x : s, y : t)'

*** Error 22.1, no typing for 'snd(x : s, y : t) : t'

*** Hint 28.9, no type match for: all

with type: '_var_6 ->? ? Unit' (line 28, column 26)

known types:

*** Hint 28.9, wrong result type '? Unit' (line 28, column 26)

for application 'all (p : ? s)'

*** Error 28.9, no typing for 'all(p : ? s) : ? Unit'

*** Hint 30.9, no type match for: And

with type: '_var_8 ->? ? Unit' (line 30, column 31)

known types:

*** Hint 30.9, wrong result type '? Unit' (line 30, column 31)

for application 'And (x : _var_7, y : ? Unit)'

*** Error 30.9, no typing for 'And(x : _var_7, y : ? Unit) : ? Unit'

*** Error 32.12, unexpected mixfix token: impl

*** Error 34.12, unexpected mixfix token: or

*** Error 34.10, unexpected pattern '__ or __ (x, y : (? Unit))'

*** Error 35.19, unexpected mixfix token: x

*** Error 34.44, unexpected mixfix token: all

*** Hint 37.3, no type match for: ex

with type: '_var_10 ->? ? Unit' (line 37, column 18)

known types:

*** Hint 37.3, wrong result type '? Unit' (line 37, column 18)

for application 'ex (p : ? s)'

*** Error 37.3, no typing for 'ex(p : ? s) : ? Unit'

*** Error 40.7, unexpected mixfix token: )

*** Error 40.3, unexpected pattern 'ff ()'

*** Error 40.20, unexpected mixfix token: all

*** Warning 61.73, data subtype ignored

*** Error 66.25, unexpected mixfix token: e

*** Error 67.12, unexpected mixfix token: e