144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitypes s, t

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop snd : s * t -> t

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x, y) = y;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x, y) = y;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x, y) = y : t;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x, y) : t = y;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x, y) : t = y;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd (x : s, y : t) : t = y;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop a : s

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram b : s = a;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop b : s

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram b : s = a;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiops x : s;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski y : t

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop c : t = snd (x : s, y : t);

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitypes

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskis : Type;

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskit : Type

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop a : s %(op)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop b : s %(op)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop c : t

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

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop snd : s * t -> t %(op)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop x : s %(op)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiop y : t %(op)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

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

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

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiprogram (var b : s) = a %(pe_b)%

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiprogram b = a %(pe_b)%

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski. c = (snd (x, y) as t) %(def_c)%

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'

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

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

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

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

88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski