sort s

op a : s

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

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

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

s : Type

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

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

a : s %(op)%

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

a = [s] a

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

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

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