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

%[ =

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

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

((var a : a), (var b : 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 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 : a; x_2 : b

. fst (Pair (x_1, x_2)) = x_1 %(ga_select_fst)%

forall a : Type; b : Type; x_1 : a; x_2 : b

. snd (Pair (x_1, x_2)) = x_2 %(ga_select_snd)%

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

%(ga_Pair)%

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

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

1.5: ### Hint: is type variable 'a'

1.8: ### Hint: is type variable 'b'

4.7: ### Warning: variable also known as type variable 'a'

4.14: ### Warning: variable also known as type variable 'b'

8.17: ### Warning: variable also known as type variable 'a'

8.20: ### Warning: variable also known as type variable 'b'

8.17: ### Warning: variable also known as type variable 'a'

8.20: ### Warning: variable also known as type variable 'b'

8.24: *** Error:

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

'[_v11_a, _v12_b]'

6.8-6.17: ### Hint:

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