Re: [mizar] structures

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

I see.

Andrzej


Freek Wiedijk wrote:

> Andrzej Trybulec wrote:
>
> >>Maybe putting this 0 or 1 in the vocabularies is better?
> >>It would be something like "Ucarrier 0" and "Utopology 1".
> >
> >You cannot have a space inside the symbol. Sorry.
>
> That's not what I meant.  It's like the priorities with the
> func symbols.  It would mean that the symbol "carrier"
> corresponds to the natural number 0.  I.e., that "the carrier
> of X = X.0" and "the topology of Y = Y.1".
>
> Freek