71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringvars a : Type; b < a

b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart Poetteringop twice2(f : a ->? b) (x : a) : ? b = f (f x);

c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringop twice3 : (a ->? b) * a ->? b =

c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering \ (f : a ->? b, x : a) . f (f x);

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart Poetteringop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart Poetteringvars f : a ->? b; x : a

f80781eaf9f927d7b4d5e66116e3f3a4242e6fa1Lennart Poettering. twice f x = f (f x);

05677bb78079c3fa0283101aac2c07581f4873f1Lennart Poetteringvars

73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poetteringa : Type %(var_1)%;

235b28269a951fdad621c5ab95c213e62df7f16eKay Sieversb < a : Type %(var_2)%

235b28269a951fdad621c5ab95c213e62df7f16eKay Sieversop twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering %[op=

539072153c0db3d91c1c59ad447d96b0e1f3cf77Lennart Poettering (\ ((var f : a ->? a))((var x : a))

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering . (var f : a ->? a) ((var f : a ->? a) (var x : a)))

35c5c7a01daeb2c83c693deea07c8f2d0d6c83e2Lennart Poettering as (a ->? b) -> a ->? b]%

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringop twice2 : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

35c5c7a01daeb2c83c693deea07c8f2d0d6c83e2Lennart Poettering %[op=

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering \ ((var f : a ->? b))((var x : a))

ddd88763921a1534081ed28e36f6712a85449005Lennart Poettering . (var f : a ->? b) ((var f : a ->? b) (var x : a)) as b]%

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringop twice3 : forall a : Type; b < a : Type . (a ->? b) * a ->? b

034a2a52ac0ec83e0229941d635d310b23eb04dfLennart Poettering %[op=

1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering (\ ((var f : a ->? b), (var x : a))

1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering . (var f : a ->? b) ((var f : a ->? b) (var x : a)))

1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering as (a ->? b) * a ->? b]%

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poetteringvars

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poetteringf : a ->? b;

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poetteringx : a

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poetteringforall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poettering %(def_twice2)%

92f30b3f05e9139c36611f6df19e87c018415edaLennart Poettering. twice3

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering = ((\ (f : a ->? b, x : a) . f (f x)) as (a ->? b) * a ->? b)

74b91131ed09850ed487a2f7849147ff6f80194dLennart Poettering %(def_twice3)%

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering. twice

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering = ((\ (f : a ->? a)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

576a01c873a79e9183292d434ec0b18af8cd36cfLennart Poettering %(def_twice)%

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringforall a : Type; b < a : Type; f : a ->? b; x : a

0a55b298d930543c8065bb9e708dd112562b1736Lennart Poettering. twice f x = f (f x)

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering### Hint 1.6, is type variable 'a'

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering### Hint 9.7, not a kind 'a ->? b'

71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering### Hint 9.20, not a class 'a'

0a55b298d930543c8065bb9e708dd112562b1736Lennart Poettering