PatternEq.hascasl.output revision 5334aa8fe0b0d1eb8a1cad40b741aa07172773c9
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtypes s, t
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettop snd : s * t -> t
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd (x, y) = y;
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd (x, y) = y;
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederprogram snd (x, y) = y : t;
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd (x, y) : t = y;
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd (x, y) : t = y;
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd (x : s, y : t) : t = y;
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachop a : s
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram b : s = a;
bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettop b : s
78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maederprogram b : s = a;
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachops x : s;
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach y : t
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachop c : t = snd (x : s, y : t);
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach%% Type Constructors -----------------------------------------------------
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachs : Type
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettt : Type
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett%% Assumptions -----------------------------------------------------------
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletta : s %(op)%
31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblettb : s %(op)%
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettc : t %(op)% = (op snd : s * t -> t) ((op x : s), (op y : t)) as t
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettsnd : s * t -> t %(op)%
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettx : s %(op)%
ae930b77ed60580110b52a09456d651f9b841883Andy Gimbletty : t %(op)%
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett%% Sentences -------------------------------------------------------------
5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%
ae930b77ed60580110b52a09456d651f9b841883Andy Gimblettprogram snd ((var x : s), (var y : t)) : t = (var y : t) : t
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett %(pe_snd)%
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd ((var x : s), (var y : t)) : t = (var y : t) %(pe_snd)%
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maederprogram snd ((var x : s) : s, (var y : t) : t) : t = (var y : t)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett %(pe_snd)%
2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettprogram (var b : s) : s = a %(pe_b)%
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram b = a %(pe_b)%
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederc = (snd (x, y) as t) %(def_c)%
0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett%% Diagnostics -----------------------------------------------------------
04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett### Hint 2.10-2.19, repeated declaration of 'snd' with type 's * t -> t'
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett*** Error 14.11-14.18, illegal toplevel pattern '((var x : s), (var y : s))'
a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly### Warning 17.10, illegal lhs pattern '(var b : s)'
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder### Hint 18.8, repeated declaration of 'b' with type 's'
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder### Hint 18.8, repeated declaration of 'b' with type 's'
6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder