Re: Re: Urelements?

Cytowanie Josef Urban <[email protected]>:

> 2012/3/14  <[email protected]>:
>> Cytowanie Josef Urban <[email protected]>:
>>
>>
>>
>> It does not matter that it is a new mechanism. It still does not work.
>>
>> Let be more precise: what yopu want to do with membership:
>>
>>
>>         let x,X be set;
>>         pred x in X;
>>
>> The membership takes structural arguments, so what Mizar is supposed to do?
>
> No, there is no structural argument in that definition.
>

So, by "takes a structural argument" you mean that the type of locus is 
structural, do you? But then, if we write

      G in X
(G - a group) it would be coerced to

      the carrier of G in X,

But if G is a family of groups, and we write

           G in X
we mean exactly what it means without any coercion.

x = y

is not coerced at all, G1 = G2 means that the group are equal

x c= y

both arguments are coreced, G1 c= G2 means     the carrier of G1 c= the 
carrier of G2

For the membership only the second argument is coerced. There are still 
some minor problems e.g. how to cope with the redefinition of the 
equality for sets

     redefine pred A = B means A c= B & B c= A

Regards,
Andrzej