Re: Element versus Subgroup

Hi:

Freek Wiedijk wrote:

>
>If I do
>
>	reserve G for Group;
>	reserve H for Subgroup of G;
>	reserve h for Element of H;
>
>(like in GROUP_2, for example), I don't think I can make
>
>	h qua Element of G
>
>work.  I think one would have to redefine the type of a
>field in a structure, or something like that, and I don't
>see how to do that.
>
>So are these thoughts correct?
>  
>
The problem is that 'Element of H' is an expandable mode, actually it is
                  Element of the carrier of H
Such a mode cannot be redefined. It had been proposed, I do not know how 
many years ago, to allow for
redefinitions of the fields of a structure. If a redefinition like
          redefine func the carrier of H -> Subset of G
were allowed, the general redefinition of an element of a non empty 
subset would work. But it is still not implemented.

Regards,
Andrzej