var s : Type

type MyPred : Type -> Type := \ s : Type . s ->? Unit

type MyAlias : Type -> Type := \ t : Type . t ->? Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a -> b -> Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a -> b -> Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a -> b -> Unit

type a2 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a -> Unit

type a3 : Type -> Type -> Type := \ (a : Type)

(a : Type) . a -> Unit

type a4 : Type -> Type -> Type := \ (a : Type)

(a : Type) . a -> Unit

type a5(a : Type)

type a5 : Type -> Type := \ a : Type . a5 a -> Unit

type a6(a : Type)

type a7 : Type -> Type := \ a : Type . a6 a -> Unit

type a6 : Type -> Type := \ a : Type . (a6 a -> Unit) -> Unit

%% Type Constructors -----------------------------------------------------

MyAlias : Type -> Type := \ t : Type . t ->? Unit

MyPred : Type -> Type := \ s : Type . s ->? Unit

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : Type := Unit

__-->__ : Type- -> Type+ -> Type

__-->?__ : Type- -> Type+ -> Type

__->__ : Type- -> Type+ -> Type

__->?__ : Type- -> Type+ -> Type

__�__ : Type+ -> Type+ -> Type

a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a -> b -> Unit

a2 : Type -> Type -> Type := \ (a : Type)(b : Type) . a -> Unit

a3 : Type -> Type -> Type := \ (a : Type)(a : Type) . a -> Unit

a4 : Type -> Type -> Type := \ (a : Type)(a : Type) . a -> Unit

a5 : Type -> Type

a6 : Type -> Type

a7 : Type -> Type := \ a : Type . a6 a -> Unit

s : Type %(var)%

%% Assumptions -----------------------------------------------------------

__/\__ : Unit � Unit ->? Unit %(Fun)%

__<=>__ : Unit � Unit ->? Unit %(Fun)%

__=__ : forall a : Type . a � a ->? Unit %(Fun)%

__=>__ : Unit � Unit ->? Unit %(Fun)%

__=e=__ : forall a : Type . a � a ->? Unit %(Fun)%

__\/__ : Unit � Unit ->? Unit %(Fun)%

__if__ : Unit � Unit ->? Unit %(Fun)%

__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

def__ : forall a : Type . a ->? Unit %(Fun)%

false : Unit %(Fun)%

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

not__ : Unit ->? Unit %(Fun)%

true : Unit %(Fun)%

%% Diagnostics -----------------------------------------------------------

*** Hint 1.5, is type variable 's'

*** Warning 6.6, redeclared type 'a1'

*** Warning 7.6, redeclared type 'a1'

*** Warning 11.19, redeclared type 'a'

*** Error 11.15, duplicates at '(11,19)' for 'a'

*** Error 13.9, duplicates at '(13,11)' for 'a'

*** Error 17.14, illegal recursive type synonym 'a5 a -> Unit'

*** Error 21.14, illegal recursive type synonym '(a6 a -> Unit) -> Unit'