Pair.hascasl.output revision 3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6
d657c51f14601d0235434ffb78cf6ac0f27cc83cLennart Poetteringvars a, b : Type
220a21d38f675eb835f5758e3d23e896573aa5eaLennart Poetteringfree type Pair a b ::= Pair (fst : a; snd : b)
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekop f(a : a; b : b) : Pair a b = Pair (a, b);
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekop g : Pair a b ->? a
78b6b7ceb2c76a3e29aeaa4b00c257be0706bffcLennart Poetteringprogram g (Pair (a, b)) = a;
78b6b7ceb2c76a3e29aeaa4b00c257be0706bffcLennart PoetteringPair : Type -> Type -> Type
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmeka : Type %(var_1)%;
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekb : Type %(var_2)%
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekop Pair : forall a : Type; b : Type . a * b -> Pair a b
4bdc60cb6fab336d455abbbd269e5bfccf760c91Lennart Poettering %(constructor)%
4bdc60cb6fab336d455abbbd269e5bfccf760c91Lennart Poetteringop f : forall a : Type; b : Type . a * b -> Pair a b
4bdc60cb6fab336d455abbbd269e5bfccf760c91Lennart Poettering \ ((var a : a), (var b : b))
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek .! (op Pair : forall a : Type; b : Type . a * b -> Pair a b)
78b6b7ceb2c76a3e29aeaa4b00c257be0706bffcLennart Poettering ((var a : a), (var b : b)) ]%
78b6b7ceb2c76a3e29aeaa4b00c257be0706bffcLennart Poetteringop fst : forall a : Type; b : Type . Pair a b -> a
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek %(selector of constructor(s)
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek Pair : forall a : Type; b : Type . a * b -> Pair a b)%
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekop g : forall a : Type; b : Type . Pair a b ->? a
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmekop snd : forall a : Type; b : Type . Pair a b -> b
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek %(selector of constructor(s)
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek Pair : forall a : Type; b : Type . a * b -> Pair a b)%
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poetteringforall a : Type; b : Type; x_1 : a; x_2 : b
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering. fst (Pair (x_1, x_2)) = x_1 %(ga_select_fst)%
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poetteringforall a : Type; b : Type; x_1 : a; x_2 : b
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering. snd (Pair (x_1, x_2)) = x_2 %(ga_select_snd)%
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poetteringfree type Pair(a : Type)(b : Type) ::= Pair (fst : a; snd : b)
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poetteringforall a : Type; b : Type; a : a; b : b . f (a, b) = Pair (a, b)
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poetteringprogram g (Pair (a, b)) = a %(pe_g)%
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering1.5: ### Hint: is type variable 'a'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering1.8: ### Hint: is type variable 'b'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering4.7: ### Warning: variable also known as type variable 'a'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering4.14: ### Warning: variable also known as type variable 'b'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering8.17: ### Warning: variable also known as type variable 'a'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering8.20: ### Warning: variable also known as type variable 'b'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering8.17: ### Warning: variable also known as type variable 'a'
4ffd29fda1a2621d8f1711ccaad723d327fef93aLennart Poettering8.20: ### Warning: variable also known as type variable 'b'
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek*** Error: in term 'program (op g : forall a : Type; b : Type . Pair a b ->? a)
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek ((op Pair : forall a : Type; b : Type . a * b -> Pair a b) (a, b))
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek are uninstantiated type variables
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek '[_v11_a, _v12_b]'
b62a309a47dd11e11729616767421397b6ca7053Zbigniew Jędrzejewski-Szmek### Hint: repeated declaration of 'g' with type 'Pair a b ->? a'