Re: [mizar] Re: Urelements?

[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?

Andrzej