Re: [mizar] Re: Urelements?

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

> It might be better to have a general syntactic mechanism ("use t(X)
> instead of X if X has some type/shape in context c") for this than an
> ad-hoc implementation for structures. One advantage would be that you
> could choose to use them or not in particular articles.

I do not believe. I think that coercions are like spice: if you use 
some, then the dish tastes good, but if you use too much of it, then it 
is not edible. So, ad hoc solution for 1-sorted structures looks O.K., 
general solution will cause a mess.