71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringvars a, b : Type

b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart Poetteringfree type Pair a b ::= Pair (fst : a; snd : b)

c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringop f(a : a; b : b) : Pair a b = Pair (a, b);

c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringop g : Pair a b ->? a

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart Poetteringprogram g (Pair (a, b)) = a;

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart Poetteringtype

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart PoetteringPair

05677bb78079c3fa0283101aac2c07581f4873f1Lennart Poettering: Type -> Type -> Type

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

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringvars

35c5c7a01daeb2c83c693deea07c8f2d0d6c83e2Lennart Poetteringa : Type %(var_1)%;

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringb : Type %(var_2)%

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

f957632b960a0a42999b38ded7089fa602b41745Kay Sievers %(constructor)%

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

f957632b960a0a42999b38ded7089fa602b41745Kay Sievers %[op=

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

9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering .! (op Pair : forall a : Type; b : Type . a * b -> Pair a b)[a, b]

9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering ((var a : a), (var b : b))

a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering as Pair a b]%

a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poetteringop fst : forall a : Type; b : Type . Pair a b -> a

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering %(selector of constructor(s)

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

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

680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poetteringop snd : forall a : Type; b : Type . Pair a b -> b

7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poettering %(selector of constructor(s)

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

c4aa65e7147dc742886edf25593e10466b02fc3aLennart Poetteringforall a : Type; b : Type; x_1_1 : a; x_1_2 : b

7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poettering. fst (Pair (x_1_1, x_1_2)) = x_1_1 %(ga_select_fst)%

7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poetteringforall a : Type; b : Type; x_1_1 : a; x_1_2 : b

7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart Poettering. snd (Pair (x_1_1, x_1_2)) = x_1_2 %(ga_select_snd)%

36e43bddd0a4526e77cdae2c922bb29f67bd74adLennart Poetteringfree type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)

36e43bddd0a4526e77cdae2c922bb29f67bd74adLennart Poettering %(ga_Pair)%

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

b61c90514e134dc781617d172961f25e7352f53bLennart Poettering %(def_f)%

b61c90514e134dc781617d172961f25e7352f53bLennart Poetteringprogram (g : Pair _v22_a _v23_b ->? _v22_a)

b61c90514e134dc781617d172961f25e7352f53bLennart Poettering ((Pair : _v22_a * _v23_b -> Pair _v22_a _v23_b) (a, b) :

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering Pair _v22_a _v23_b)

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering : _v22_a

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering = a %(pe_g)%

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering*** Error 8.24, in term 'program (op g : forall a : Type; b : Type . Pair a b ->? a)[_v22_a,

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering _v23_b]

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering ((op Pair : forall a : Type; b : Type . a * b -> Pair a b)[_v22_a,

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering _v23_b]

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering (a, b))

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering = a'

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering are uninstantiated type variables '[_v22_a, _v23_b]'

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

a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering