types s, t < t

ops a, b : s

%% op __ + __ : s -> s -> s, idem, assoc, comm;

op __+__ : s * s -> s

op __+__ : t * t -> t

op __+__ : t -> t -> t

ops a, b : t

op c : s = a + b;

op d : s = a + a : s;

op e : s * s -> s = __+__;

op f : s * s -> s = __+__;

op g : s * s = (a, b);

op h : s = a + b;

op i : s = (a : s) + (b : s);

op incr : s -> s

op i1 : s = incr a;

op i2 : s = incr a;

op i3 : s = incr a;

op __<=__<=__ : s * s * s -> s

op l1 : s = a <= b <= c;

op l2 : s * s * s -> s = __<=__<=__;

op l3 : s = a <= b <= c;

op l4 : s = a <= b <= c;

op l5 : s * s * s = (a, b, c);

op x : s

op y : s = (op a : s) <= (var x : s) <= (a : s);

op z : s = (x as s) + (x as t as s);

. x in s %(bla_label)%

. x in t;

types

s : Type;

t : Type

type

s < t

op __+__ : t -> t -> t

op __+__ : s * s -> s

op __+__ : t * t -> t

op __<=__<=__ : s * s * s -> s

op a : s

op a : t

op b : s

op b : t

op c : s %[ = (op __+__ : s * s -> s) ((op a : s), (op b : s)) ]%

op d : s

%[ = (op __+__ : s * s -> s) ((op a : s), (op a : s)) : s ]%

op e : s * s -> s %[ = (op __+__ : s * s -> s) ]%

op f : s * s -> s %[ = (op __+__ : s * s -> s) ]%

op g : s * s %[ = ((op a : s), (op b : s)) ]%

op h : s %[ = (op __+__ : s * s -> s) ((op a : s), (op b : s)) ]%

op i : s %[ = (op __+__ : s * s -> s) ((op a : s), (op b : s)) ]%

op i1 : s %[ = (op incr : s -> s) (op a : s) ]%

op i2 : s %[ = (op incr : s -> s) (op a : s) ]%

op i3 : s %[ = (op incr : s -> s) (op a : s) ]%

op incr : s -> s

op l1 : s

%[ =

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s)) ]%

op l2 : s * s * s -> s %[ = (op __<=__<=__ : s * s * s -> s) ]%

op l3 : s

%[ =

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s)) ]%

op l4 : s

%[ =

(op __<=__<=__ : s * s * s -> s)

((op a : s), (op b : s), (op c : s)) ]%

op l5 : s * s * s %[ = ((op a : s), (op b : s), (op c : s)) ]%

op x : s

op y : s

%[ =

(op __<=__<=__ : s * s * s -> s)

((op a : s), (var x : s), (op a : s)) ]%

op z : s

%[ = (op __+__ : s * s -> s) ((op x : s), (op x : s) as s) ]%

. c = (op __+__ : s * s -> s) (a, b)

. d = ((op __+__ : s * s -> s) (a, a) : s)

. e = (op __+__ : s * s -> s)

. f = (op __+__ : s * s -> s)

. g = (a, b)

. h = (op __+__ : s * s -> s) (a, b)

. i = (op __+__ : s * s -> s) (a, b)

. i1 = incr a

. i2 = incr a

. i3 = incr a

. l1 = a <= b <= c

. l2 = __<=__<=__

. l3 = a <= b <= c

. l4 = a <= b <= c

. l5 = (a, b, c)

forall x : s . y = a <= (var x : s) <= a

. z = (op __+__ : s * s -> s) (x, x as s)

. true %(bla_label)%

. true

7.14: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

7.14: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

8.14: ### Hint:

no kind found for 't'

expected: {Cpo}

found: {Type}

8.14: ### Hint:

no kind found for 't'

expected: {Cppo}

found: {Type}

9.4-9.10: ### Warning: expected tuple argument for '__+__'

13.12-13.16: ### Hint:

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (3.12)

13.12-13.16: ### Hint: untypeable term (with type: t) '(a, b)'

15.14-15.20: ### Hint:

in type of '((op a : s), (op a : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (3.12)

15.14-15.20: ### Hint: untypeable term (with type: t) '(a, a)'

15.14-15.20: ### Hint:

rejected 't < s' of '(op __+__ : t * t -> t) ((op a : s), (op a : s))'

17.8: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

17.8: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

17.6-17.24: ### Hint:

in type of '(op __+__ : t -> t -> t) as s * s -> s'

typename 't' (9.14)

is not unifiable with type 's * s' (17.12)

19.8: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

19.8: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

19.6-19.25: ### Hint:

in type of '(op __+__ : t -> t -> t) as s * s -> s'

typename 't' (9.14)

is not unifiable with type 's * s' (19.12)

21.8: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

21.8: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

23.23-23.26: ### Hint:

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (3.12)

23.23-23.26: ### Hint: untypeable term (with type: t) '(a, b)'

25.23-25.30: ### Hint:

in type of '((op a : s), (op b : s))'

typename 't' (9.14)

is not unifiable with type 's * s' (25.34)

25.23-25.32: ### Hint:

untypeable term (with type: t) '(a : s, b : s)'

34.21: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

34.21: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

37.9: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

37.9: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

40.9: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

40.9: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

46.14-46.34: ### Hint:

in type of '((op x : s) as s, (op x : s) as t as s)'

typename 't' (9.14)

is not unifiable with type 's * s' (46.37)

46.14-46.34: ### Hint:

untypeable term (with type: t) '(x as s, x as t as s)'