2fbe4699ac5d2a8bafe8c0c8aa41e6717d36d5ceChristian Maedervars a : Type; b < a

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maederop twice2(f : a ->? b) (x : a) : ? b = f (f x);

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederop twice3 : (a ->? b) * a ->? b =

a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder \ (f : a ->? b, x : a) . f (f x);

a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

2fbe4699ac5d2a8bafe8c0c8aa41e6717d36d5ceChristian Maedervars f : a ->? b; x : a

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder. twice f x = f (f x);

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedervars

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedera : Type %(var_1)%;

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederb < a : Type %(var_2)%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder %[ =

e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder \ f : a ->? b; x : a

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a)) ]%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop twice2 : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder %[ =

f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder \ f : a ->? b; x : a

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a)) ]%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop twice3 : forall a : Type; b < a : Type . (a ->? b) * a ->? b

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder %[ =

e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder \ ((var f : a ->? b), (var x : a))

678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a)) ]%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedervars

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederf : a ->? b;

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

c4280f2006756af8b2c102e390e5c46c9c1a612fChristian Maederforall a : Type; b < a : Type; f : a ->? b; x : a

e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder. twice2 f x = f (f x)

c4280f2006756af8b2c102e390e5c46c9c1a612fChristian Maederforall a : Type; b < a : Type

e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder. twice3 = \ (f : a ->? b, x : a) . f (f x)

c4280f2006756af8b2c102e390e5c46c9c1a612fChristian Maederforall a : Type; b < a : Type

e4f3c121d197ca18cd8f67deaabdddf7f6bdb7e9Christian Maeder. twice = \ (f : a ->? b)(x : a) . f (f x)

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederforall a : Type; b < a : Type; f : a ->? b; x : a

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. twice f x = f (f x)

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder1.6: ### Hint: is type variable 'a'

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder5.14-5.20: ### Hint:

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maederno kind found for 'a ->? b'

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder expected: {Cpo}

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder found: {Type}

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder5.14-5.20: ### Hint:

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maederno kind found for 'a ->? b'

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder expected: {Cppo}

5de34eba726f63d1522bf17a857309a6208ce0b5Christian Maeder found: {Type}

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder9.7: ### Hint: not a kind 'a ->? b'

3aa7e4492a7e28b37d1a0b23f5bfe2109f87d4d6Christian Maeder9.20: ### Hint: not a class 'a'