01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder%% Type Constructors -----------------------------------------------------

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLogical : Type := Unit ->? Unit

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiUnit : Type

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder__*__ : +Type -> +Type -> Type

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

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder__->?__ : -Type -> +Type -> Type

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder%% Assumptions -----------------------------------------------------------

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

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

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski__if__ : ? Unit * ? Unit ->? Unit %(fun)%

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder__when__else__

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

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

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

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederfalse : Unit %(fun)%

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedernot__ : ? Unit ->? Unit %(fun)%

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maedertrue : Unit %(fun)%

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

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder%% Diagnostics -----------------------------------------------------------

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder*** Warning 1.3-1.13, trying hard to find lazy type for '(\ . ())()'

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder*** Hint 1.4-1.6, in type of '(\ . ()) : _var_2_v2'

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski typename 'Unit'

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang is not unifiable with type '_var_1_v1 ->? Unit'

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder*** Hint 1.3-1.13, untypable application (with result type: Unit)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder '(\ . ())()'

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder*** Error 1.3-1.13, no typing for '(\ . ())()'

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang