XUnion.hascasl.output revision d48085f765fca838c1d972d2123601997174583d
var S : Type; N : Type; E : Type
type Set : Type -> Type := \ S : Type . S_v-1 ->? Unit
type Graph : Type -> Type -> Type := \ (N : Type)(E : Type) . (Set
N_v-1)@(N_v-1 ->? Unit)
* (E_v-2 ->? N_v-1) *
(E_v-2 ->? N_v-1)
op __union__ : Graph N E * Graph N E -> Graph N E;
__union__, __intersection__, __\\__ : Set S * Set S -> Set S
forall g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N));
g' : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N))
. ((fun __=__[(N ->? Unit) * (E ->? N) * (E ->? N)]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
((N ->? Unit) * (E ->? N) * (E ->? N)) *
((N ->? Unit) * (E ->? N) * (E ->? N))
->? Unit)
(((op __union__[N; E]
: forall N : Type; E : Type .
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
*
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
->
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))) :
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)) *
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N))
-> (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)))
(var g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N)),
var g' : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N))) :
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)),
var g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N))) :
Unit
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Graph
: Type -> Type -> Type
:= \ (N : Type)(E : Type) . (Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1)
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Set : Type -> Type := \ S : Type . S_v-1 ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
__-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
%% Type Variables --------------------------------------------------------
E : Type %(var_3)%
N : Type %(var_2)%
S : Type %(var_1)%
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__\\__
: forall S : Type .
(Set S_v-1)@(S_v-1 ->? Unit) * (Set S_v-1)@(S_v-1 ->? Unit) ->
(Set S_v-1)@(S_v-1 ->? Unit)
%(op)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__intersection__
: forall S : Type .
(Set S_v-1)@(S_v-1 ->? Unit) * (Set S_v-1)@(S_v-1 ->? Unit) ->
(Set S_v-1)@(S_v-1 ->? Unit)
%(op)%
__union__
: forall S : Type .
(Set S_v-1)@(S_v-1 ->? Unit) * (Set S_v-1)@(S_v-1 ->? Unit) ->
(Set S_v-1)@(S_v-1 ->? Unit)
%(op)%
: forall N : Type; E : Type .
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
*
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
->
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
%(op)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
true : Unit %(fun)%
�__ : ? Unit ->? Unit %(fun)%
%% Variables -------------------------------------------------------------
g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N))
g' : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N))
%% Sentences -------------------------------------------------------------
((fun __=__[(N ->? Unit) * (E ->? N) * (E ->? N)]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
((N ->? Unit) * (E ->? N) * (E ->? N)) *
((N ->? Unit) * (E ->? N) * (E ->? N))
->? Unit)
(((op __union__[N; E]
: forall N : Type; E : Type .
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
*
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))
->
(Graph N_v-1 E_v-2)@((Set N_v-1)@(N_v-1 ->? Unit) *
(E_v-2 ->? N_v-1) * (E_v-2 ->? N_v-1))) :
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)) *
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N))
-> (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)))
(var g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N)),
var g' : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N))) :
(Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) * (E ->? N)),
var g : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N))) :
Unit
%% 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)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N)),
var g' : (Graph N E)@((Set N)@(N ->? Unit) * (E ->? N) *
(E ->? N)))'
typename '__->?__'
is not unifiable with type '__*__*__ ((Set N)@(N ->? Unit))' (8.23)