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

pred tt : s

var x : s

program (pred tt : s) = \ (var x : s) . ()

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

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

pred eq : s * s

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

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) = all (\ r : (? Unit) . r ())

forall x : t; y : t

. %(..)%

(fun __=__[t] : 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 < Data2 %[type __ ::=

a : -> __

b : -> __

c : -> __]%

Data2 : Type %[type __ ::=

Cons21 : Data1 * Data2 -> __

Cons22 : Data2 * 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 -----------------------------------------------------------

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

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

program (pred tt : s) = \ (var x : s) . () %(pe_tt)%

(fun __=__[t] : forall a : Type . a * a ->? Unit)

(var x : t, var y : t)

type Data1 (|-> Data1) ::=

a : -> __

b : -> __

c : -> __ %(ga_Data1)%

type Data2 (|-> Data2) ::=

Cons21 : Data1 * Data2 -> __

Cons22 : Data2 * Data1 -> __ %(ga_Data2)%

type Data3 (|-> Data3) ::=

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

Cons32 : Data2 *

Data1 -> __ (sel2 :? Data2)(sel1 :? Data1) %(ga_Data3)%

type Data4 (|-> Data4) ::=

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

Cons42 : Data2 *

Data1 ->? __ (sel2 :? Data2)(sel1 :? Data1) %(ga_Data4)%

(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

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

with type: '_var_3 ->? s' (21.20)

known types:

*** Hint 21.1, wrong result type 's' (21.20)

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

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

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

with type: '_var_4 ->? t' (22.20)

known types:

*** Hint 22.1, wrong result type 't' (22.20)

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

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

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

with type: '_var_5 ->? ? Unit' (28.27)

known types:

*** Hint 28.9, wrong result type '? Unit' (28.27)

for application 'all(var p : ? s)'

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

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

with type: '_var_7 ->? ? Unit' (30.32)

known types:

*** Hint 30.9, wrong result type '? Unit' (30.32)

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

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

*** Error 32.12, unexpected mixfix token: impl

*** Error 34.12, unexpected mixfix token: or

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

with type: '_var_8 ->? ? Unit' (37.19)

known types:

*** Hint 37.3, wrong result type '? Unit' (37.19)

for application 'ex(var p : ? s)'

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

*** Hint 40.3, no type match for: ff

with type: '_var_9 ->? ? Unit' (40.12)

known types:

*** Hint 40.3, wrong result type '? Unit' (40.12)

for application 'ff()'

*** Error 40.3, no typing for 'ff() : ? Unit'

*** Error 66.25, unexpected mixfix token: e

*** Error 67.12, unexpected mixfix token: e