class Type < Type;

var t : Type

class 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 tt = \ x : s . ();

program

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

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

pred eq : s * s

type s < ? s

program

program

program

program

forall x : t; y : t

%(..)%

. x = y;

sort 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)?

. true;

forall x : s

forall x : s

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

TYPE < Type

a < b

b < Type

c < Type

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

Data1

: Type < Data2

%[type Data1 ::=

a : Data1

b : Data1

c : Data1]%

Data2

: Type

%[type Data2 ::=

Cons21 : Data1 * Data2 -> Data2(Data1; Data2)

Cons22 : Data2 * Data1 -> Data2(Data2; Data1)

types Data1]%

Data3

: Type

%[type Data3 ::=

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

Cons32 : Data2 * Data1 -> Data3(sel2 :? Data2; sel1 :? Data1)]%

Data4

: Type

%[type Data4 ::=

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

Cons42 : Data2 * Data1 ->? Data4(sel2 :? Data2; sel1 :? Data1)]%

s : (Type, c)

%% Type Variables --------------------------------------------------------

t : Type %(var_1)%

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

a

: Data1 %(construct Data1)%

: ? s %(op)%

b : Data1 %(construct Data1)%

c : Data1 %(construct Data1)%

eq : s * s ->? Unit %(pred)%

fst : s * t ->? s %(op)%

sel1

: Data4 ->? Data1

%(select from Data4 constructed by

(Cons42 : Data2 * Data1 ->? Data4,

Cons41 : Data1 * Data2 ->? Data4))%

: Data3 ->? Data1

%(select from Data3 constructed by

(Cons32 : Data2 * Data1 -> Data3,

Cons31 : Data1 * Data2 -> Data3))%

sel2

: Data4 ->? Data2

%(select from Data4 constructed by

(Cons42 : Data2 * Data1 ->? Data4,

Cons41 : Data1 * Data2 ->? Data4))%

: Data3 ->? Data2

%(select from Data3 constructed by

(Cons32 : Data2 * Data1 -> Data3,

Cons31 : Data1 * Data2 -> Data3))%

snd : s * t ->? t %(op)%

tt : s ->? Unit %(pred)%

%% Variables -------------------------------------------------------------

x : s

y : t

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

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

program (var fst : s * t ->? s) (x, y : t) : s = x %(pe_fst)%

program (var snd : s * t ->? t) (x, y : t) : t = y %(pe_snd)%

x = y

type Data1 ::=

a : Data1

b : Data1

c : Data1 %(ga_Data1)%

type Data2 ::=

Cons21 : Data1 * Data2 -> Data2(Data1; Data2)

Cons22 : Data2 * Data1 -> Data2(Data2; Data1)

types Data1 %(ga_Data2)%

forall x_1_1 : Data1; x_1_2 : Data2 .

(op sel1 : Data3 ->? Data1) (Cons31 (x_1_1, x_1_2)) = x_1_1

%(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2 .

(op sel2 : Data3 ->? Data2) (Cons31 (x_1_1, x_1_2)) = x_1_2

%(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1 .

(op sel2 : Data3 ->? Data2) (Cons32 (x_1_1, x_1_2)) = x_1_1

%(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1 .

(op sel1 : Data3 ->? Data1) (Cons32 (x_1_1, x_1_2)) = x_1_2

%(ga_select_sel1)%

type Data3 ::=

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

Cons32 : Data2 * Data1 -> Data3(sel2 :? Data2; sel1 :? Data1)

%(ga_Data3)%

forall x_1_1 : Data1; x_1_2 : Data2 .

(op sel1 : Data4 ->? Data1) (Cons41 (x_1_1, x_1_2)) = x_1_1

%(ga_select_sel1)%

forall x_1_1 : Data1; x_1_2 : Data2 .

(op sel2 : Data4 ->? Data2) (Cons41 (x_1_1, x_1_2)) = x_1_2

%(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1 .

(op sel2 : Data4 ->? Data2) (Cons42 (x_1_1, x_1_2)) = x_1_1

%(ga_select_sel2)%

forall x_1_1 : Data2; x_1_2 : Data1 .

(op sel1 : Data4 ->? Data1) (Cons42 (x_1_1, x_1_2)) = x_1_2

%(ga_select_sel1)%

type Data4 ::=

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

Cons42 : Data2 * Data1 ->? Data4(sel2 :? Data2; sel1 :? Data1)

%(ga_Data4)%

true

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

### Warning 1.7, void universe class declaration 'Type'

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

*** Error 7.11, illegal type pattern argument '__'

*** Error 11.16, not a class 'd'

### Warning 11.7, unchanged class 'a'

### Warning 11.10, unchanged class 'b'

### Warning 11.13, unchanged class 'c'

### Hint 11.19, refined class 'a'

### Hint 16.7, not a class 's'

### Hint 18.15, rebound variable 'x'

*** Error 20.12, unexpected mixfix token: res

### Hint 21.6, rebound variable 'x'

### Hint 21.6, rebound variable 'x'

### Warning 21.5-21.16, illegal lhs pattern '(var fst : s * t ->? s) ((var x : s), (var y : t))'

### Hint 22.6, rebound variable 'x'

### Hint 22.6, rebound variable 'x'

### Warning 22.5-22.16, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'

### Hint 28.41, in type of '(p, (pred tt : s))'

typename 's' (24.15)

is not unifiable with type 's ->? Unit' (15.11)

### Hint 28.35-28.41, untypable application (with result type: ? Unit)

'eq (p, tt)'

*** Error 28.33, no typing for 'program all (p : ? s) : ? Unit = eq (p, tt)'

### Hint 30.14, rebound variable 'x'

### Hint 30.40, no type match for: t1

with (maximal) type: _v64 ->? _v63 ->? _v62 ->? _v61 ->? ? Unit

known types:

### Hint 30.40-30.42, untypable application (with result type: _v63 ->? _v62 ->? _v61 ->? ? Unit)

't1'

### Hint 30.40-30.45, untypable application (with result type: _v62 ->? _v61 ->? ? Unit)

't1 res'

### Hint 30.40-30.49, untypable application (with result type: _v61 ->? ? Unit)

't1 res t2'

### Hint 30.40-30.52, untypable application (with result type: ? Unit)

't1 res t2 ()'

*** Error 30.38, no typing for 'program And (x, y : ? Unit) : ? Unit = t1 res t2 ()'

*** Error 32.12, unexpected mixfix token: impl

*** Error 34.12, unexpected mixfix token: or

### Hint 37.27, no type match for: all

with (maximal) type: _v74 ->? ? Unit

known types:

### Hint 37.27-38.45, untypable application (with result type: ? Unit)

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

*** Error 37.25, no typing for 'program ex (p : ? s) : ? Unit =

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

### Hint 40.20, no type match for: all

with (maximal) type: _v82 ->? ? Unit

known types:

### Hint 40.20-40.38, untypable application (with result type: ? Unit)

'all (\ r : ? Unit . r)'

*** Error 40.18, no typing for 'program ff () : ? Unit = all (\ r : ? Unit . r)'

### Hint 45.9, not a class 't'

### Hint 45.8, rebound variable 'x'

### Hint 45.16, not a class 't'

### Hint 57.11, redeclared type 's'

### Hint 66.22, not a class 's'

### Hint 66.21, rebound variable 'x'

### Hint 66.25, no type match for: e

with (maximal) type: Unit

known types:

*** Error 66.25, no typing for 'e'

### Hint 67.9, not a class 's'

### Hint 67.8, rebound variable 'x'

### Hint 67.12, no type match for: e

with (maximal) type: Unit

known types:

*** Error 67.12, no typing for 'e'