9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervars a, b : Type

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop f(a : a; b : b) : Pair a b = Pair (a, b);

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop g : Pair a b ->? a

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederprogram g (Pair (a, b)) = a;

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedertype

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederPair : Type -> Type -> Type

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedervars

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedera : Type %(var_1)%;

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederb : Type %(var_2)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop Pair : forall a : Type; b : Type . a * b -> Pair a b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder %(constructor)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop f : forall a : Type; b : Type . a * b -> Pair a b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder %[op=

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder \ ((var a : a), (var b : b))

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ((var a : a), (var b : b))

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder as Pair a b]%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop fst : forall a : Type; b : Type . Pair a b -> a

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder %(selector of constructor(s)

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop g : forall a : Type; b : Type . Pair a b ->? a %(op)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederop snd : forall a : Type; b : Type . Pair a b -> b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder %(selector of constructor(s)

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederforall a : Type; b : Type; x_1 : a; x_2 : b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder. fst (Pair (x_1, x_2)) = x_1 %(ga_select_fst)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederforall a : Type; b : Type; x_1 : a; x_2 : b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder. snd (Pair (x_1, x_2)) = x_2 %(ga_select_snd)%

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

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder %(ga_Pair)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederforall a : Type; b : Type; a : a; b : b

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder. f (a, b) = (Pair (a, b) as Pair a b)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederprogram g (Pair (a, b)) = a %(pe_g)%

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 1.5, is type variable 'a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 1.8, is type variable 'b'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 4.7, variable also known as type variable 'a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 4.14, variable also known as type variable 'b'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 8.17, variable also known as type variable 'a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 8.20, variable also known as type variable 'b'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 8.17, variable also known as type variable 'a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Warning 8.20, variable also known as type variable 'b'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder*** Error 8.24,

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederin term 'program (op g : forall a : Type; b : Type . Pair a b ->? a)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ((op Pair : forall a : Type; b : Type . a * b -> Pair a b) (a, b))

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder = a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder are uninstantiated type variables

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder'[_v19_a, _v20_b]'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder### Hint 6.8-6.17,

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederrepeated declaration of 'g' with type 'Pair a b ->? a'

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder