Re: Re: Urelements?

[email protected]
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[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.

> 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.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.