Element versus Subgroup

[Freek Wiedijk]

Dear all,

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?

And if one would do structures in the Lee/Rudnicki way,
would this be different?

Freek

[Piotr Rudnicki]

Freek,

I have hoped that someone would answer your question by now.  I have heard
from the Bialystok people that either what you want is undoable or some
special "gymnastics" is need.  No evidence though.

In the alternative approach to structures there should be no problem as we
really do not have structures.  I would have to implement it before being
sure.


Best,

--
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr


On Wed, Oct 22, 2008 at 06:32:32PM +0200, Freek Wiedijk wrote:

> Dear all,
>
> 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?
>
> And if one would do structures in the Lee/Rudnicki way,
> would this be different?
>
> Freek

[trybulec]

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
                   

[Freek Wiedijk]

Dear Andrzej,

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

I see.  Thanks for the answer!

Freek