vars a, b : Type

free type Pair a b ::= Pair (fst : a; snd : b)

op f(a : a; b : b) : Pair a b = Pair (a, b);

op g : Pair a b ->? a

program g (Pair (a, b)) = a;

type

Pair : Type -> Type -> Type

vars

a : Type %(var_1)%;

b : Type %(var_2)%

op Pair : forall a : Type; b : Type . a * b -> Pair a b

%(constructor)%

op f : forall a : Type; b : Type . a * b -> Pair a b

%[op=

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

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

((var a : a), (var b : b))

as Pair a b]%

op fst : forall a : Type; b : Type . Pair a b -> a

%(selector of constructor(s)

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

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

op snd : forall a : Type; b : Type . Pair a b -> b

%(selector of constructor(s)

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

forall a : Type; b : Type; x_1_1 : a; x_1_2 : b

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

forall a : Type; b : Type; x_1_1 : a; x_1_2 : b

. snd (Pair (x_1_1, x_1_2)) = x_1_2 %(ga_select_snd)%

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

%(ga_Pair)%

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

program g (Pair (a, b)) = a %(pe_g)%

*** Error 8.24,

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

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

= a'

are uninstantiated type variables

'[_v19_a, _v20_b]'

### Hint 6.8-6.17,

repeated declaration of 'g' with type 'Pair a b ->? a'