8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovavars S, N, E : Type

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovatype Set S := S ->? Unit

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovatype Graph N E := Set N * (E ->? N) * (E ->? N)

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakovaops __union__ : Graph N E * Graph N E -> Graph N E;

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova __union__, __intersection__, __\\__ : Set S * Set S -> Set S

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakovaforall g, g' : Graph N E . g union g' = g;

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%% Type Constructors -----------------------------------------------------

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaGraph : Type -> Type -> Type := \ N : Type . _t7

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaSet : Type -> Type := \ S : Type . S ->? Unit

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

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%% Type Variables --------------------------------------------------------

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaE : Type %(var_3)%

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaN : Type %(var_2)%

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina SojakovaS : Type %(var_1)%

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%% Assumptions -----------------------------------------------------------

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

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

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova__union__

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

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

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%(op)%

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%% Variables -------------------------------------------------------------

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovag : Graph N E

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakovag' : Graph N E

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova%% Sentences -------------------------------------------------------------

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

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova%% Diagnostics -----------------------------------------------------------

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 1.7, is type variable 'S'

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 1.9, is type variable 'N'

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 1.11, is type variable 'E'

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 8.11, not a kind 'Graph N E'

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova### Hint 8.15, not a kind 'Graph N E'

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

b5702fcfbabcc2b13557bc96ed8376133420dc73Kristina Sojakova type 'Graph N' (8.23)

8b054cade993ef373d564b2d74c9c5a2da48f8b7Kristina Sojakova is not unifiable with type '\ S : Type . S ->? Unit' (2.23)

9d770d1ea15092156d65e2a89b081eeeb8c6b153Kristina Sojakova

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova