[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] structures



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