Re: [mizar] Re: Urelements?

[Josef Urban <josef.urban@gmail.com>]

2012/3/14  <trybulec@math.uwb.edu.pl>:
> Cytowanie Josef Urban <josef.urban@gmail.com>:
>
>
>> 2012/3/13  <trybulec@math.uwb.edu.pl>:
>>>
>>> Cytowanie Josef Urban <josef.urban@gmail.com>:
>>>
>>>
>>>>
>>>> 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?

No, there is no structural argument in that definition.

Josef

>
> Andrzej
>
>