66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maedersort s, t

81d182b21020b815887e9057959228546cf61b6bChristian Maederop snd : s * t -> t

81d182b21020b815887e9057959228546cf61b6bChristian Maederprogram snd (x, y) = y;

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederprogram snd (x, y) = y;

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederprogram snd (x, y) = y : t;

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maederprogram snd (x, y) : t = y;

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederprogram snd (x, y) : t = y;

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maederprogram snd (x : s, y : t) : t = y;

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederprogram

66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maederop a : s

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederprogram b : s = a;

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederop b : s

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederprogram b : s = a;

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederop x : s;

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder y : t

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

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder%% Type Constructors -----------------------------------------------------

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeders : Type

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maedert : Type

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder%% Assumptions -----------------------------------------------------------

5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maedera : s %(op)%

fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederb : s %(op)%

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

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedersnd : s * t -> t %(op)%

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederx : s %(op)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedery : t %(op)%

59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder%% Sentences -------------------------------------------------------------

05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederprogram snd ((var x : s), (var y : t)) : t = (var y : t) : t

5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder %(pe_snd)%

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

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

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederprogram snd ((var x : s) : s, (var y : t) : t) : t = (var y : t)

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder %(pe_snd)%

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederprogram (var b : s) : s = a %(pe_b)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederprogram b = a %(pe_b)%

f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederc = (snd (x, y) as t) %(def_c)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%% Diagnostics -----------------------------------------------------------

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

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

946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder