2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maedervar a : Type; b < a

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederop twice2 : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? b))((var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

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

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? b), (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder as (a ->? b) * a ->? b

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederop twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? a))((var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? a) ((var f : a ->? a) (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder as (a ->? b) -> a ->? b

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

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder. (fun __=__[b] : forall a : Type . a * a ->? Unit)

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder ((((op twice[a; b] :

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder forall a : Type; b < a : Type . (a ->? b) -> a ->? b)

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder (var f : a ->? b))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder (var x : a),

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian 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)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertwice

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder %(op)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? a))((var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? a) ((var f : a ->? a) (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder as (a ->? b) -> a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maedertwice2

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder %(op)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? b))((var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

01996e191c1a9a2251abf7740124b73bde771472Christian Maedertwice3

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder : forall a : Type; b < a : Type . (a ->? b) * a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder %(op)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder = \ ((var f : a ->? b), (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . (var f : a ->? b) ((var f : a ->? b) (var x : a))

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder as (a ->? b) * a ->? b

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

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

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

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

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

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder . ((twice2 (f)) x) = (f (f (x)) as b) %(def_twice2)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maedertwice3 =

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder(\ (f, x) . f (f (x)) as (a ->? b) * a ->? b) %(def_twice3)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maedertwice =

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder(\ (f)(x) . f (f (x)) as (a ->? b) -> a ->? b) %(def_twice)%

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder((twice (f)) x) = (f (f (x)))

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder*** Hint 1.6, is type variable 'a'

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder*** Hint 9.7, not a kind 'a ->? b'

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder*** Hint 9.20, not a class 'a'