Re: Re: Urelements?
| 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.