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

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

Hi Jesse,

On Wed, 29 Nov 2006, Jesse Alama wrote:

> Andrzej Trybulec <trybulec@math.uwb.edu.pl> writes:
>
> > you probably need in the Environment Declaration
> >
> >   registrations FRAENKEL;
>
> Why?

Because the registrations in FRAENKEL ensure that the type Element of 
Funcs(A,B) widens to the "type" Function. "Function" is actually just 
syntactic sugar ("expandable mode") for attributes Function-like and 
Relation-like (http://mmlquery.mizar.org/mml/4.66.942/funct_1.html#NM1).

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).

Best,
Josef