649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaclass Type

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksavar t : Type

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaclass TYPE

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksatype Unit : TYPE

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaclasses a, b, c

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaclasses a, b, c;

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa a < b

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksatype s : c

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksapred tt : s

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksavar x : s

649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksaprogram 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 ::=

Cons21 (Data1; Data2) | Cons22 (Data2; Data1) | types 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 %(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 | b | c %(ga_Data1)%

type Data2 ::=

Cons21 (Data1; Data2) | Cons22 (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 (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'

*** 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 26.6, redeclared type 's'

### 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: Unit ->? _v62 ->? _v61 ->? Unit ->? ? Unit

known types:

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

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

known types:

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

't1 ()'

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

't1 () res'

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

't1 () res t2'

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

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

known types:

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

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

known types:

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

't1 ()'

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

't1 () res'

### Hint 30.40-30.49, untypable application (with result type: ? (? 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: _v81 ->? ? Unit

known types:

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

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

### Hint 40.3, rebound variable 'ff'

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