Re: Re: Urelements?

Cytowanie Josef Urban <[email protected]>:

> 2012/3/13  <[email protected]>:
>> Cytowanie Josef Urban <[email protected]>:
>>
>>
>>>
>>> Why not use the type info that you already have? If a
>>> functor/predicate takes a structural argument, use it. If not, use the
>>> structure's carrier.
>>>
>>
>> If a locus has the type 'set', then it takes any argument, also structural.
>> If structures are sets.
>
> I does not matter, this is a new mechanism.
>


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?

Andrzej