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 Constructors -----------------------------------------------------

Pair

: Type -> Type -> Type

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

%% Type Variables --------------------------------------------------------

a : Type %(var_1)%

b : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

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

%(constructor)%

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

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)%

g : forall a : Type; b : Type . Pair a b ->? a %(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)%

%% Sentences -------------------------------------------------------------

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)

%(def_f)%

program (g : Pair _v25 _v27_b ->? _v25)

((Pair : _v25 * _v27_b -> Pair _v25 _v27_b) (a, b) :

Pair _v25 _v27_b)

: _v25

= a %(pe_g)%

%% Diagnostics -----------------------------------------------------------

*** 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 '[_v25, _v27_b]'

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