class Type

var t : Type

class TYPE

type Unit : TYPE

classes a, b, c

classes a, b, c;

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;

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

. true;

forall x : s

forall x : s

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

TYPE < Type

a < b

b < Type

c < Type

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

Data1 : Type < Data2 %[type Data1 ::= a | b | c]%

Data2

: Type

%[type Data2 ::=

types Data1 | Cons21 (Data1; Data2) | Cons22 (Data2; Data1)]%

Data3

: Type

%[type Data3 ::=

Cons31 (sel1 :? Data1; sel2 :? Data2) |

Cons32 (sel2 :? Data2; sel1 :? Data1)]%

Data4

: Type

%[type Data4 ::=

Cons41 (sel1 :? Data1; sel2 :? Data2)? |

Cons42 (sel2 :? Data2; sel1 :? Data1)?]%

s : c

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

t : Type %(var_1)%

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

Cons21 : Data1 * Data2 -> Data2 %(constructor)%

Cons22 : Data2 * Data1 -> Data2 %(constructor)%

Cons31 : Data1 * Data2 -> Data3 %(constructor)%

Cons32 : Data2 * Data1 -> Data3 %(constructor)%

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

Cons42 : Data2 * Data1 ->? Data4 %(constructor)%

a : Data1 %(constructor)%

a : ? s %(op)%

b : Data1 %(constructor)%

c : Data1 %(constructor)%

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

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

sel1 : Data3 ->? Data1

%(selector of constructor(s)

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

sel1 : Data4 ->? Data1

%(selector of constructor(s)

(Cons41 : Data1 * Data2 ->? Data4,

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

sel2 : Data3 ->? Data2

%(selector of constructor(s)

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

sel2 : Data4 ->? Data2

%(selector of constructor(s)

(Cons41 : Data1 * Data2 ->? Data4,

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

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 | b | c %(ga_Data1)%

type Data2 ::=

types Data1 | Cons21 (Data1; Data2) | Cons22 (Data2; 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 (sel1 :? Data1; sel2 :? Data2) |

Cons32 (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 (sel1 :? Data1; sel2 :? Data2)? |

Cons42 (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'

### Hint 15.11, repeated declaration of 'tt' with type 's ->? Unit'

*** Error 20.12, unexpected mixfix token: res

### Hint 21.6, rebound variable 'x'

### Hint 21.6, rebound variable 'x'

### Warning 21.1-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.1-22.16, illegal lhs pattern '(var snd : s * t ->? t) ((var x : s), (var y : t))'

### Hint 26.6, redeclared type 's'

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

typename 's' (24.15)

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

### Hint 28.38-28.41, untypable term (with type: s * s)

'(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 found for 't1'

### Hint 30.40, no type found for 't1'

### Hint 30.40, untypable term (with type: ? (_v50 ->? _v49 ->? Unit ->? ? Unit))

't1'

### Hint 30.40-30.42, untypable term (with type: _v50 ->? _v49 ->? Unit ->? ? Unit)

't1 ()'

### Hint 30.40-30.45, untypable term (with type: _v49 ->? Unit ->? ? Unit)

't1 () res'

### Hint 30.40, no type found for 't1'

### Hint 30.40, no type found for 't1'

### Hint 30.40, untypable term (with type: ? (_v52 ->? _v51 ->? ? (? Unit)))

't1'

### Hint 30.40-30.42, untypable term (with type: _v52 ->? _v51 ->? ? (? Unit))

't1 ()'

### Hint 30.40-30.45, untypable term (with type: _v51 ->? ? (? Unit))

't1 () res'

### Hint 30.40-30.49, untypable term (with 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 found for 'all'

### Hint 37.27, untypable term (with type: _v62 ->? ? Unit)

'all'

*** 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 found for 'all'

### Hint 40.20, untypable term (with type: _v69 ->? ? Unit)

'all'

### Hint 40.3, rebound variable 'ff'

### Hint 40.20, no type found for 'all'

### Hint 40.20, untypable term (with type: _v70 ->? ? Unit)

'all'

*** 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 62.11-62.70, repeated declaration of 'sel2' with type 'Data3 ->? Data2'

### Hint 62.11-63.1, repeated declaration of 'sel1' with type 'Data3 ->? Data1'

### Hint 64.11-64.71, repeated declaration of 'sel2' with type 'Data4 ->? Data2'

### Hint 64.11-64.84, repeated declaration of 'sel1' with type 'Data4 ->? Data1'

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

### Hint 66.21, rebound variable 'x'

### Hint 66.25, no type found for 'e'

*** 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 found for 'e'

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