bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maedertype s

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederop a : s

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederop __=[s]__ : forall a . a * a -> Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder. ((op __=[s]__[s] : forall a : Type . a * a -> Unit) :

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s * s -> Unit)

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder (op a : s, op a : s) :

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder%% Type Constructors -----------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder? : +Type -> Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederLogical : Type := ? Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit

488aed6214197096d0e23c9bbd614263b11a543bJonathan von SchroederUnit : Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder__*__ : +Type -> +Type -> Type

488aed6214197096d0e23c9bbd614263b11a543bJonathan von Schroeder__*__*__ : +Type -> +Type -> +Type -> Type

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

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

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

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

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

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

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeders : Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder%% Assumptions -----------------------------------------------------------

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

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

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__=[s]__ : forall a : Type . a * a -> Unit %(op)%

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

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

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

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

__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

a : s %(op)%

bottom : forall a : Type . a %(fun)%

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

false : Unit %(fun)%

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

true : Unit %(fun)%

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

%% Sentences -------------------------------------------------------------

(__=[s]__ : s * s -> Unit)(a, a) : Unit

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

*** Warning 4.22, missing kind for type variable 'a'

*** Warning 6.28, missing kind for type variable 'a'