2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maedervar a : Type; b < a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederop twice2 : forall a : Type; b < a : Type . (a ->? b) -> a ->? b =

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederop twice3 : forall a : Type; b < a : Type . (a ->? b) * a ->? b =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder \ ((var f : a ->? b), (var x : a)) .

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder as (a ->? b) * a ->? b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederop twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder \ ((var f : a ->? a))((var x : a)) .

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder as (a ->? b) -> a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maedervar f : a ->? b; x : a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder. (op twice[a; b] :

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder forall a : Type; b < a : Type . (a ->? b) -> a ->? b)

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (var x : a)

9df7943e174665a367e75714d54b352a3760dd58Christian Maeder = (var f : a ->? b) ((var f : a ->? b) (var x : a))

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Type Constructors -----------------------------------------------------

d48085f765fca838c1d972d2123601997174583dChristian Maeder? : +Type -> Type

d48085f765fca838c1d972d2123601997174583dChristian MaederLogical : Type := ? Unit

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederUnit : Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__*__ : +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->?__ : -Type -> +Type -> Type

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

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedera : Type %(var_1)%

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederbottom : forall a : Type . a %(fun)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederfalse : Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedernot__ : ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertrue : Unit %(fun)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\ ((var f : a ->? a))((var x : a)) .

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice2

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice3

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder: forall a : Type; b < a : Type . (a ->? b) * a ->? b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder\ ((var f : a ->? b), (var x : a)) .

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder�__ : ? Unit ->? Unit %(fun)%

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

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice2)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice3 = (\ (f : a ->? b, x : a) . f (f x) as (a ->? b) * a ->? b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice3)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian 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'