Re: [mizar] Re: Urelements?

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

If there is one use-case, somebody will find another.

Also note that for structures their opaque implementation is why their
members are irrelevant. If we knew that they are partial functions,
things would be different. So this is related to the problem of
treating pairs abstractly or concretely.

Best,
Josef





>
>
>
>