a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype s, t

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblettop snd : s � t -> t

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd : s � t -> t (x : s, y : t) = (var y : t)

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd : s � t -> t (x : s, y : t) = (var y : t)

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederprogram snd : s � t -> t (x : s, y : t) = (var y : t) : t

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd : s � t -> t (x : s, y : t) : t = (var y : t)

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram snd : s � t -> t (x : s, y : t) : t = (var y : t)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram snd : s � t -> t (x : s, y : t) : t = (var y : t)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachprogram (x : s, y : s) = (x : s, y : s)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachop a : s

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettprogram b : s = a

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettop b : s

78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maederprogram b : s : s = (op a : s)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachop x : s; y : t

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachop c : t = (op snd : s � t -> t) ((op x : s) : s, (op y : t) : t)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach%% Type Constructors -----------------------------------------------------

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPred : Type -> Type := \ a : Type . a ->? Unit

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachUnit : Type := Unit

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett__-->__ : Type- -> Type+ -> Type

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett__-->?__ : Type- -> Type+ -> Type

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett__->__ : Type- -> Type+ -> Type

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett__->?__ : Type- -> Type+ -> Type

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett__�__ : Type+ -> Type+ -> Type

5b5db1d788d5240070930175f1322dab56279f99Andy Gimbletts : Type

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblettt : Type

ae930b77ed60580110b52a09456d651f9b841883Andy Gimblett%% Assumptions -----------------------------------------------------------

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett__/\__ : Unit � Unit ->? Unit %(Fun)%

5b5db1d788d5240070930175f1322dab56279f99Andy Gimblett__<=>__ : Unit � Unit ->? Unit %(Fun)%

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach__=__ : forall a : Type . a � a ->? Unit %(Fun)%

ae930b77ed60580110b52a09456d651f9b841883Andy Gimblett__=>__ : Unit � Unit ->? Unit %(Fun)%

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach__\/__ : Unit � Unit ->? Unit %(Fun)%

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach__if__ : Unit � Unit ->? Unit %(Fun)%

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimbletta : s %(Op)%

2f615f62c47e2c0ae9964f37f5bac6905d86f475Andy Gimblettb : s %(Op)% = (op a : s)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachc : t %(Op)% = (op snd : s � t -> t) ((op x : s) : s,

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder (op y : t) : t)

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblettdef__ : forall a : Type . a ->? Unit %(Fun)%

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblettfalse : Unit %(Fun)%

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettif__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettnot__ : Unit ->? Unit %(Fun)%

06dd4e7c29f33f6122a910719e3bd9062256e397Andy Gimblettsnd : s � t -> t %(Op)% = \ (x : s, y : t) . (var y : t)

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimbletttrue : Unit %(Fun)%

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettx : s %(Op)%

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimbletty : t %(Op)%

a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly%% Diagnostics -----------------------------------------------------------

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder*** Warning 6.10, different terms of 'snd'

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder \ (x : s, y : t) . (var y : t)

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder \ (x : s, y : t) . (var y : t) : t

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder*** Error 14.10, illegal toplevel pattern '(x : s, y : s)'

6caa773a17aa8cb5b6196abbd5ede98ef01beb8aChristian Maeder*** Error 17.9, illegal toplevel pattern 'b : s'

a65b135c4ed7e68b2510bc218018ffa8f9a34fe8Liam O'Reilly