Rules for usage of a colon before the label
Boris Schminke <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
Dear All, Why some of the labels need to start with a colon, e. g. definition let X be set; attr X is empty means :Def1: not ex x being set st x in X; end; After deleting the colon in this situation we will receive error messages: ::> 143: No implicit qualification ::> 321: Predicate symbol or "is" expected On the other hand, if I add a colon before a label in more usual case I will see messages like theese: ::> 391: Incorrect beginning of a text item ::> 396: Formula expected It seems to me that it is a strict rule only for labels just before the definiens, isn't it? Yours, Schminke Boris.