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

Re: [mizar] structures



Hi Josef,

>We can choose well-ordered ("SelOrder") infinite set of selectors 
>("Selectors"), and then define e.g.:
>
>definition
>func carrier equals SelOrder(0);
>synonym Objects;
>synonym Vertices;
>func topology equals SelOrder(1);
>end;

Maybe putting this 0 or 1 in the vocabularies is better?
It would be something like "Ucarrier 0" and "Utopology 1".

Freek