type s

op a : s

vars a, b : Type

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

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

. a =[s] a

. a =e=[s : Type] a;

op f[a] : a -> Unit

op g[b,a] : a * b -> Unit

op h[b,a] : a -> b

op j[a,b] : a -> b

class Funct < Type -> Type

vars f, F : Funct

%% order of var declarations counts

op k[a,f] : f a

op k[b,a,f] : b -> f a

op k[a,b,f] : b -> f a

op l[F,a] : F a

%% or explicit forall order

op k[G,b,a] : forall G : Funct; b : Type; a : Type . b -> G a

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

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

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

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

op if__then__else[a][a : Type]__ : a * a * a -> a

op if__then__else[s][a : Type]__ : a * a * a -> a

op if__then__else[a : Type]__ : a * a * a -> a

class

Funct < Type -> Type

type

s : Type

vars

F : Funct %(var_20)%;

a : Type %(var_1)%;

b : Type %(var_2)%;

f : Funct %(var_19)%

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

op a : s %(op)%

op f[a] : forall a : Type . a -> Unit %(op)%

op g[b,a] : forall a : Type; b : Type . a * b -> Unit %(op)%

op h[b,a] : forall a : Type; b : Type . a -> b %(op)%

op if__then__else__ : forall a : Type . a * a * a -> a %(op)%

op if__then__else[a]__ : forall a : Type . a * a * a -> a %(op)%

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

op j[a,b] : forall a : Type; b : Type . a -> b %(op)%

op k[G,b,a] : forall G : Funct; b : Type; a : Type . b -> G a

%(op)%

op k[a,b,f] : forall a : Type; b : Type; f : Funct . b -> f a

%(op)%

op k[a,f] : forall a : Type; f : Funct . f a %(op)%

op k[b,a,f] : forall a : Type; b : Type; f : Funct . b -> f a

%(op)%

op l[F,a] : forall a : Type; F : Funct . F a %(op)%

. a =[s] a

. a =[s] a

. a =e= a

. a =[s] a

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

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

. a =[s] a

### Hint 4.5, is type variable 'a'

### Hint 4.8, is type variable 'b'

### Hint 6.6-6.9, is polymorphic compound identifier '__=[s]__'

### Hint 8.9-8.12, is polymorphic compound identifier '__=[s]__'

### Hint 10.6-10.8, is compound list '[s]'

### Hint 11.8-11.15, is type list '[s : Type]'

### Hint 13.4-13.7, is polymorphic compound identifier 'f[a]'

### Warning 15.6, unexpected identifier in compound list 'b'

### Hint 15.4-15.9, is polymorphic compound identifier 'g[b,a]'

### Warning 17.6, unexpected identifier in compound list 'b'

### Hint 17.4-17.9, is polymorphic compound identifier 'h[b,a]'

### Warning 19.8, unexpected identifier in compound list 'b'

### Hint 19.4-19.9, is polymorphic compound identifier 'j[a,b]'

### Hint 23.5, is type variable 'f'

### Hint 23.8, is type variable 'F'

### Warning 25.9, unexpected identifier in compound list 'f'

### Hint 25.4-25.10, is polymorphic compound identifier 'k[a,f]'

### Warning 26.6, unexpected identifier in compound list 'b'

### Warning 26.12, unexpected identifier in compound list 'f'

### Hint 26.4-26.13, is polymorphic compound identifier 'k[b,a,f]'

### Warning 27.9, unexpected identifier in compound list 'b'

### Warning 27.12, unexpected identifier in compound list 'f'

### Hint 27.4-27.13, is polymorphic compound identifier 'k[a,b,f]'

### Warning 29.6, unexpected identifier in compound list 'F'

### Hint 29.4-29.10, is polymorphic compound identifier 'l[F,a]'

### Hint 32.34, rebound type variable 'b'

### Hint 32.37, rebound type variable 'a'

### Warning 32.6, unexpected identifier in compound list 'G'

### Warning 32.9, unexpected identifier in compound list 'b'

### Hint 32.4-32.13, is polymorphic compound identifier 'k[G,b,a]'

### Hint 34.44, is type list '[s]'

### Hint 34.9-34.12, is polymorphic compound identifier '__=[s]__'

### Hint 35.44-35.46, is type list '[s, s]'

### Hint 35.9-35.12, is polymorphic compound identifier '__=[s]__'

### Hint 35.44-35.46,

for type scheme 'a * a -> Unit' wrong length of instantiation list

'[s, s]'

### Hint 35.4-35.16,

untypeable term (with type: _v30 ->? Unit)

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

*** Error 35.4-35.53,

no typing for

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

### Hint 36.7-36.9, is compound list '[s]'

### Hint 36.10-36.22, is type list '[s, s : Type]'

### Hint 36.11-36.16,

for type scheme 'a * a -> Unit' wrong length of instantiation list

'[s, s : Type]'

### Hint 36.6-36.22, no type found for '__=[s]__'

### Hint 36.6-36.26,

untypeable term (with type: _v31 ->? Unit)

'__ =[s][s, s : Type] __ : s * s -> Unit'

*** Error 36.3-36.47,

no typing for '(__ =[s][s, s : Type] __ : s * s -> Unit) (a, a)'

### Hint 37.7-37.9, is compound list '[s]'

### Hint 37.29-37.31, is compound list '[s]'

*** Error 37.30, unexpected mixfix token: s

### Hint 38.7-38.9, is compound list '[s]'

### Hint 38.10-38.12, is compound list '[s]'

### Hint 38.32-38.34, is compound list '[s]'

*** Error 38.10, unexpected mixfix token: [

### Hint 39.7-39.9, is compound list '[s]'

### Hint 40.7-40.9, is compound list '[s]'

### Hint 40.10-40.19, is type list '[s : Type]'

### Hint 41.43, is type list '[s]'

### Hint 41.14, rebound type variable 'a'

### Hint 41.9-41.12, is polymorphic compound identifier '__=[s]__'

### Hint 43.22, rebound type variable 'a'

### Hint 43.4-43.20,

is polymorphic compound identifier 'if__then__else[a]__'

### Hint 44.22, rebound type variable 'a'

### Hint 44.4-44.20,

is polymorphic compound identifier 'if__then__else[s]__'

### Hint 45.19, rebound type variable 'a'