6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithclass Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithvar t : Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithclass TYPE

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype Unit : TYPE

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithclasses a, b, c

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithclasses a, b, c;

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith a < b

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype s : c

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithpred tt : s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithvar x : s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram tt = \ x : s . ();

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithfst (x : s, y : t) : s = x;

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithsnd (x : s, y : t) : t = y;

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithpred eq : s * s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype s < ? s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithprogram

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithforall x : t; y : t

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith%(..)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith. x = y;

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithop a : (? s)

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype Data1 ::= a | b | c

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype Data2

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ::= Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | type Data1

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype Data3

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith Cons32 (sel2 :? Data2; sel1 :? Data1)

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithtype Data4

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith Cons42 (sel2 :? Data2; sel1 :? Data1)?

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith. true;

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithforall x : s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithforall x : s

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith%% Classes ---------------------------------------------------------------

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John SmithTYPE < Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smitha < b

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithb < Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithc < Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith%% Type Constructors -----------------------------------------------------

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

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John SmithData2

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith: Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith %[type Data2 ::=

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith types Data1 | Cons21 (Data1; Data2) | Cons22 (Data2; Data1)]%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John SmithData3

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith: Type

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis %[type Data3 ::=

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith Cons31 (sel1 :? Data1; sel2 :? Data2) |

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

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisData4

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis: Type

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith %[type Data4 ::=

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis Cons41 (sel1 :? Data1; sel2 :? Data2)? |

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

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavaniss : c

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith%% Type Variables --------------------------------------------------------

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanist : Type %(var_1)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis%% Assumptions -----------------------------------------------------------

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisCons21 : Data1 * Data2 -> Data2 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisCons22 : Data2 * Data1 -> Data2 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisCons31 : Data1 * Data2 -> Data3 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisCons32 : Data2 * Data1 -> Data3 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex ValavanisCons41 : Data1 * Data2 ->? Data4 %(constructor)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John SmithCons42 : Data2 * Data1 ->? Data4 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanisa : Data1 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanisa : ? s %(op)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanisb : Data1 %(constructor)%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithc : Data1 %(constructor)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavaniseq : s * s ->? Unit %(pred)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanisfst : s * t ->? s %(op)%

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanissel1 : Data3 ->? Data1

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis %(selector of constructor(s)

20e25114cc4b04c88faf68f0f3e19dc13833474aAlex Valavanis (Cons31 : Data1 * Data2 -> Data3,

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith Cons32 : Data2 * Data1 -> Data3))%

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smithsel1 : Data4 ->? Data1

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith %(selector of constructor(s)

6bd7ac3b4704cf1cba90dd21a73bfedd6d640a16John Smith (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.9-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'