vars S, N, E : Type

type Set S := S ->? Unit

type Graph N E := Set N * (E ->? N) * (E ->? N)

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

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

forall g, g' : Graph N E . g union g' = g;

types

Graph : Type -> Type -> Type;

Set : Type -> Type

types

Graph (N : Type) (E : Type) := Set N * (E ->? N) * (E ->? N);

Set (S : Type) := S ->? Unit

vars

E : Type %(var_3)%;

N : Type %(var_2)%;

S : Type %(var_1)%

op __\\__ : 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 __union__ : forall N : Type; E : Type

. Graph N E * Graph N E -> Graph N E

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

. (op __union__ :

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

(g, g')

= g

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

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

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

3.21-3.25: ### Hint:

no kind found for 'Set N'

expected: {Cpo}

found: {Type}

3.21-3.25: ### Hint:

no kind found for 'Set N'

expected: {Cppo}

found: {Type}

5.20-5.28: ### Hint:

no kind found for 'Graph N E'

expected: {Cpo}

found: {Type}

5.20-5.28: ### Hint:

no kind found for 'Graph N E'

expected: {Cppo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cpo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cppo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cpo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cppo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cpo}

found: {Type}

6.47-6.51: ### Hint:

no kind found for 'Set S'

expected: {Cppo}

found: {Type}

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

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

9.6-9.14: ### Hint:

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

typename '__->?__' (2.19)

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

9.6-9.14: ### Hint:

untypeable term (with type: Set _v8_S * Set _v8_S) '(g, g')'