Re: [mizar] Element versus Subgroup

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

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