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;

program

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)%

op b : s %(op)%

op c : t

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

op snd : s * t -> t %(op)%

op x : s %(op)%

op y : t %(op)%

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) as t) %(def_c)%

### Hint 2.10-2.19,

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

### Hint 2.10-2.19,

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

### Hint 2.10-2.19,

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

### Hint 2.10-2.19,

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

### Hint 2.10-2.19,

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

### Hint 2.10-2.19,

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

*** Error 14.10-14.18,

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

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

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

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