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