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

op x : s;

y : t

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

%% Type Constructors -----------------------------------------------------

s : Type

t : Type

%% Assumptions -----------------------------------------------------------

a : s %(op)%

b : s %(op)%

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

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

x : s %(op)%

y : t %(op)%

%% Sentences -------------------------------------------------------------

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) : 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) : s, (var y : t) : t) : t = (var y : t)

%(pe_snd)%

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

program b = a %(pe_b)%

c = (snd (x, y) as t) %(def_c)%

%% Diagnostics -----------------------------------------------------------

*** Error 14.11-14.18, illegal toplevel pattern '((var x : s), (var y : s))'

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