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

((x : s) res (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

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 < Type;

b < Type;

c < Type

class

a < b

types

Data1 : Type;

Data2 : Type;

Data3 : Type;

Data4 : Type;

Unit : TYPE;

s : c

type

Data1 < Data2

var

t : Type %(var_1)%

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

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

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

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

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

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

op a : Data1 %(constructor)%

op a : ? s

op b : Data1 %(constructor)%

op c : Data1 %(constructor)%

op fst : s * t ->? s

op sel1 : Data3 ->? Data1

%(selector of constructor(s)

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

op sel1 : Data4 ->? Data1

%(selector of constructor(s)

(Cons41 : Data1 * Data2 ->? Data4,

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

op sel2 : Data3 ->? Data2

%(selector of constructor(s)

(Cons31 : Data1 * Data2 -> Data3,

Cons32 : Data2 * Data1 -> Data3))%

op sel2 : Data4 ->? Data2

%(selector of constructor(s)

(Cons41 : Data1 * Data2 ->? Data4,

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

op snd : s * t ->? t

pred eq : s * s

pred tt : s

var

x : s

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

program (x res y) : s = x %(pe___res__)%

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

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

forall t : Type; x : t; y : t . x = y

type Data1 ::= a | b | c %(ga_Data1)%

type Data2 ::=

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

%(ga_Data2)%

forall x_1 : Data1; x_2 : Data2

. (op sel1 : Data3 ->? Data1) (Cons31 (x_1, x_2)) = x_1

%(ga_select_sel1)%

forall x_1 : Data1; x_2 : Data2

. (op sel2 : Data3 ->? Data2) (Cons31 (x_1, x_2)) = x_2

%(ga_select_sel2)%

forall x_1 : Data2; x_2 : Data1

. (op sel2 : Data3 ->? Data2) (Cons32 (x_1, x_2)) = x_1

%(ga_select_sel2)%

forall x_1 : Data2; x_2 : Data1

. (op sel1 : Data3 ->? Data1) (Cons32 (x_1, x_2)) = x_2

%(ga_select_sel1)%

type Data3 ::=

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

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

forall x_1 : Data1; x_2 : Data2

. (op sel1 : Data4 ->? Data1) (Cons41 (x_1, x_2)) = x_1

%(ga_select_sel1)%

forall x_1 : Data1; x_2 : Data2

. (op sel2 : Data4 ->? Data2) (Cons41 (x_1, x_2)) = x_2

%(ga_select_sel2)%

forall x_1 : Data2; x_2 : Data1

. (op sel2 : Data4 ->? Data2) (Cons42 (x_1, x_2)) = x_1

%(ga_select_sel2)%

forall x_1 : Data2; x_2 : Data1

. (op sel1 : Data4 ->? Data1) (Cons42 (x_1, x_2)) = x_2

%(ga_select_sel1)%

type Data4 ::=

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

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

. true

1.7-1.10: ### Warning: void universe class declaration 'Type'

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

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

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

11.7: ### Warning: unchanged class 'a'

11.10: ### Warning: unchanged class 'b'

11.13: ### Warning: unchanged class 'c'

11.19: ### Warning: refined class 'a'

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

18.15: ### Hint: rebound variable 'x'

15.9-15.11: ### Hint:

repeated declaration of 'tt' with type 's ->? Unit'

20.19: ### Hint: rebound variable 'x'

20.19: ### Hint: rebound variable 'x'

20.10-20.15: ### Warning:

ignoring declaration for builtin identifier '__res__'

20.12-20.31: ### Warning:

illegal lhs pattern '((var x : s) res (var y : t)) : s'

21.6: ### Hint: rebound variable 'x'

21.6: ### Hint: rebound variable 'x'

21.1-21.18: ### Warning:

illegal lhs pattern

'(var fst : s * t ->? s) ((var x : s), (var y : t)) : s'

22.6: ### Hint: rebound variable 'x'

22.6: ### Hint: rebound variable 'x'

22.1-22.18: ### Warning:

illegal lhs pattern

'(var snd : s * t ->? t) ((var x : s), (var y : t)) : t'

24.11: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {c}

24.11: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {c}

26.6: ### Hint: redeclared type 's'

28.41: ### Hint:

in type of '(pred tt : s)'

typename 's' (24.15)

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

28.38-28.41: ### Hint: untypeable term (with type: s * s) '(p, tt)'

28.33: *** Error:

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

30.14: ### Hint: rebound variable 'x'

30.40-30.41: ### Hint: no type found for 't1'

30.40: ### Hint: untypeable term 't1'

30.40-30.49: ### Hint:

untypeable term (with type: ? _v35_a * ? _v36_b) '(t1 (), t2 ())'

30.38: *** Error:

no typing for

'program And (x, y : ? Unit) : ? Unit = t1 () res t2 ()'

32.12: *** Error: unexpected mixfix token: impl

34.12: *** Error: unexpected mixfix token: or

37.27-37.29: ### Hint: no type found for 'all'

37.27: ### Hint: untypeable term 'all'

37.25: *** Error:

no typing for

'program ex (p : ? s) : ? Unit

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

40.20-40.22: ### Hint: no type found for 'all'

40.20: ### Hint: untypeable term 'all'

40.18: *** Error:

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

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

45.8: ### Hint: rebound variable 'x'

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

57.11: ### Hint: redeclared type 's'

62.11-62.70: ### Hint:

repeated declaration of 'sel2' with type 'Data3 ->? Data2'

62.11-63.1: ### Hint:

repeated declaration of 'sel1' with type 'Data3 ->? Data1'

64.11-64.71: ### Hint:

repeated declaration of 'sel2' with type 'Data4 ->? Data2'

64.11-64.84: ### Hint:

repeated declaration of 'sel1' with type 'Data4 ->? Data1'

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

66.21: ### Hint: rebound variable 'x'

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

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

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

67.8: ### Hint: rebound variable 'x'

67.12: ### Hint: no type found for 'e'

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