b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedervar a : Type; b < a

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederop twice2(f : a ->? b)(x : a) :? b = f (f x)

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

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder \ (f : a ->? b, x : a) . f (f x)

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedervar f : a ->? b; x : a

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder. twice f x = f (f x)

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder%% Type Variables --------------------------------------------------------

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedera : Type %(var_1)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederb < a : Type %(var_2)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Assumptions -----------------------------------------------------------

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maedertwice

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder%(op)% =

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder(\ ((var f : a ->? a))((var x : a)) .

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder (var f : a ->? a) ((var f : a ->? a) (var x : a)))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederas (a ->? b) -> a ->? b

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maedertwice2

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder%(op)% =

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder\ ((var f : a ->? b))((var x : a)) .

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder(var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maedertwice3

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) * a ->? b

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maeder%(op)% =

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder(\ ((var f : a ->? b), (var x : a)) .

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder (var f : a ->? b) ((var f : a ->? b) (var x : a)))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederas (a ->? b) * a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Variables -------------------------------------------------------------

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Sentences -------------------------------------------------------------

2f2237571ed7885b0f1ccb2c17996e8922f3d12dChristian Maederforall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice2)%

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maedertwice3 =

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder((\ (f : a ->? b, x : a) . f (f x)) as (a ->? b) * a ->? b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice3)%

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maedertwice = ((\ (f)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice)%

c7041924e85535e80c7c08699cb308071d7010beChristian Maedertwice f x = f (f x)

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Diagnostics -----------------------------------------------------------

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 1.6, is type variable 'a'

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 9.7, not a kind 'a ->? b'

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 9.20, not a class 'a'