types s, t

op snd : s * t -> t

program snd (x, y) = y;

program snd (x, y) = y;

program snd (x, y) = y : t;

program snd (x, y) : t = y;

program snd (x, y) : t = y;

program snd (x : s, y : t) : t = y;

op a : s

program b : s = a;

op b : s

program b : s = a;

ops x : s;

y : t

op c : t = snd (x : s, y : t);

types

s : Type;

t : Type

op a : s

op b : s

op c : t %[ = (op snd : s * t -> t) ((op x : s), (op y : t)) ]%

op snd : s * t -> t

op x : s

op y : t

program snd ((var x : s), (var y : t)) = (var y : t) %(pe_snd)%

program snd ((var x : s), (var y : t)) = (var y : t) %(pe_snd)%

program snd ((var x : s), (var y : t)) = (var y : t) %(pe_snd)%

program snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

program snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

program snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

program (var b : s) = a %(pe_b)%

program b = a %(pe_b)%

. c = snd (x, y)

2.10: ### Hint:

no kind found for 's'

expected: {Cpo}

found: {Type}

2.10: ### Hint:

no kind found for 's'

expected: {Cppo}

found: {Type}

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

2.10-2.19: ### Hint:

repeated declaration of 'snd' with type 's * t -> t'

14.10-14.16: *** Error:

illegal toplevel pattern '((var x : s), (var y : s))'

17.9-17.10: ### Warning: illegal lhs pattern '(var b : s)'

18.8: ### Hint: repeated declaration of 'b' with type 's'

18.8: ### Hint: repeated declaration of 'b' with type 's'