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
