class Type < Type

var t : Type

class TYPE < {x . x < t}

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

class a, b, c < Type

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

type s : c

op 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

op 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

. %(..)%

(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 < {x . x < t}

a < b

b < Type

c < Type

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

Unit : TYPE := Unit

s : c < ? 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 = \ x : s . ()

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

Error (line 7, column 6) incompatible kind of: Pred

expected: Type -> Type

found: Type- -> Type

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

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