c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedervar a : Type; b : Type

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederop twice : (a ->? b) -> a ->? b

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder %% = \ (f : a ->? b) (x : a) . f(f(x))

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederLogical : Type := Unit ->? Unit

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederUnit : Type

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

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

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

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedera : Type %(var_1)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederb : Type %(var_2)%

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

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__when__else__

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederbottom : forall a : Type . a_v-1 %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederfalse : Unit %(fun)%

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertrue : Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertwice

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder : forall a : Type; b : Type . (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder %(op)%

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

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

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

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder*** Error, unbound type variable(s)

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder a : Type in 'a_v1'