2b873214c9ab511bbca437c036371ab664aedaceChristian Maedervars a, b : Type

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederfree type Pair a b ::= Pair (fst : a; snd : b)

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maederop f(a : a; b : b) : Pair a b = Pair (a, b);

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maederop g : Pair a b ->? a

54ed6a6b1a6c7d27fadb39ec5b59d0806c81f7c8Christian Maederprogram g (Pair (a, b)) = a;

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski%% Type Constructors -----------------------------------------------------

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederPair

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski: Type -> Type -> Type

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski %[free type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)]%

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder%% Type Variables --------------------------------------------------------

c092fcac4b8f5c524c22ca579189c4487c13edf7Christian Maedera : Type %(var_1)%

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederb : Type %(var_2)%

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder%% Assumptions -----------------------------------------------------------

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederPair : forall a : Type; b : Type . a * b -> Pair a b

da955132262baab309a50fdffe228c9efe68251dCui Jian %(constructor)%

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederf : forall a : Type; b : Type . a * b -> Pair a b

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maeder %(op)% =

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder \ ((var a : a), (var b : b))

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder .! (op Pair : forall a : Type; b : Type . a * b -> Pair a b)

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder ((var a : a), (var b : b))

0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder as Pair a b

52d922076b89f12234f721974e82531bc69a6f69Christian Maederfst : forall a : Type; b : Type . Pair a b -> a

52d922076b89f12234f721974e82531bc69a6f69Christian Maeder %(selector of constructor(s)

43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder Pair : forall a : Type; b : Type . a * b -> Pair a b)%

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maederg : forall a : Type; b : Type . Pair a b ->? a %(op)%

91eeff7b19b22d7e5c5d83fa6e357496e291c718Christian Maedersnd : forall a : Type; b : Type . Pair a b -> b

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder %(selector of constructor(s)

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder Pair : forall a : Type; b : Type . a * b -> Pair a b)%

fbc4f8708092d571a45cb483f37cc6b674da45a7Christian Maeder%% Sentences -------------------------------------------------------------

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskiforall a : Type; b : Type; x_1_1 : a; x_1_2 : b

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maeder. fst (Pair (x_1_1, x_1_2)) = x_1_1 %(ga_select_fst)%

dda5ab793f1615c1ba1dcaa97a4346b0878da6b1Christian Maederforall a : Type; b : Type; x_1_1 : a; x_1_2 : b

9175e29c044318498a40f323f189f9dfd50378efChristian Maeder. snd (Pair (x_1_1, x_1_2)) = x_1_2 %(ga_select_snd)%

f77f29e84b3f6e791c82e61b13fbf76582bedd2fChristian Maederfree type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)

f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder %(ga_Pair)%

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederforall a : a; b : b . f (a, b) = (Pair (a, b) as Pair a b)

da333ffa6336cf59a4071fcddad358c5eafd3e61Sonja Gröning %(def_f)%

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederprogram (g : Pair _v22_a _v23_b ->? _v22_a)

6352f3c31da3043783a13be6594aacb2147378baRazvan Pascanu ((Pair : _v22_a * _v23_b -> Pair _v22_a _v23_b) (a, b) :

8ef91a173e69219fc2ebd45c76a35891c7785abdMarkus Gross Pair _v22_a _v23_b)

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder : _v22_a

a2b04db3e156312a8596d8084f7f0f51acf8a96bChristian Maeder = a %(pe_g)%

0c885f1348fd58f7cb706472a3ff20b52dbef0a7Jonathan von Schroeder%% Diagnostics -----------------------------------------------------------

fc1a590cd3ee36797c0a032ff41e07f8e2469341Christian Maeder*** Error 8.24, in term 'program (op g : forall a : Type; b : Type . Pair a b ->? a)

66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu ((op Pair : forall a : Type; b : Type . a * b -> Pair a b) (a, b))

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross = a'

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder are uninstantiated type variables '[_v22_a, _v23_b]'

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder### Hint 6.8-6.17, repeated declaration of 'g' with type 'Pair a b ->? a'

d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder