Re: [mizar] Re: a term representing the extension of a type

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Wed, 29 Nov 2006, Josef Urban wrote:

> When you import the needed registrations from FRAENKEL, i.e.
>
> registration let A, B be set;
> cluster Funcs(A,B) -> functional;
> end;
>
> registration let P be functional set;
>  cluster -> Function-like Relation-like Element of P;
> end;
>
> the attribute "functional" will be automatically added to any "Funcs(A,B)" 
> term, and the attributes "Function-like" and  "Relation-like" will be 
> automatically added to any term which already has the "functional" attribute, 
> making it a "Function" (needed for the "." functor).

sorry, I should have written:
... the attributes "Function-like" and  "Relation-like" will be 
automatically added to any term of type "Element of P", where P is a term 
which already has the "functional" attribute ...

Josef