var S : Type; N : Type; E : Type

type Set : Type -> Type := \ S : Type . S ->? Unit

type Graph : Type -> Type -> Type

:= \ (N : Type)(E : Type) . Set N * (E ->? N) * (E ->? N)

op __union__ : Graph N E * Graph N E -> Graph N E;

__union__, __intersection__, __\\__ : Set S * Set S -> Set S

forall g : Graph N E; g' : Graph N E

. (op __union__[N; E] :

forall N : Type; E : Type . Graph N E * Graph N E -> Graph N E)

((var g : Graph N E), (var g' : Graph N E))

= (var g : Graph N E)

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

Graph

: Type -> Type -> Type

:= \ (N : Type)(E : Type) . Set N * (E ->? N) * (E ->? N)

Set : Type -> Type := \ S : Type . S ->? Unit

%% Type Variables --------------------------------------------------------

E : Type %(var_3)%

N : Type %(var_2)%

S : Type %(var_1)%

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

__\\__ : forall S : Type . Set S * Set S -> Set S %(op)%

__intersection__ : forall S : Type . Set S * Set S -> Set S %(op)%

__union__

: forall S : Type . Set S * Set S -> Set S %(op)%

: forall N : Type; E : Type . Graph N E * Graph N E -> Graph N E

%(op)%

%% Variables -------------------------------------------------------------

g : Graph N E

g' : Graph N E

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

(__union__ : Graph N E * Graph N E -> Graph N E) (g, g') = g

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

### Hint 1.7, is type variable 'S'

### Hint 1.9, is type variable 'N'

### Hint 1.11, is type variable 'E'

### Hint 2.12, rebound type variable 'S'

### Hint 3.14, rebound type variable 'N'

### Hint 3.16, rebound type variable 'E'

### Hint 8.11, not a kind 'Graph N E'

### Hint 8.15, not a kind 'Graph N E'

### Hint, in type of '((var g : Graph N E), (var g' : Graph N E))'

typename '__->?__'

is not unifiable with type '__*__*__ (Set N)' (8.23)