Correct, you cannot have any x$) within a comment. From the PDF (p. 139): "Comments have the following syntax:
"$( *text* $) "Here, *text* is a string, possibly empty, of any characters in Metamath’s character set (p. 112), except that the character strings $( and $) may not appear in *text*." Since every token in a Metamath database outside a comment falls under the three token kinds (except perhaps for included filenames which still act like math symbols), and no token kind allows $ except at the start of keywords, x$) can appear nowhere in a compliant database. Matthew House On Sat, Oct 4, 2025, 5:52 AM Igor Ieskov <[email protected]> wrote: > Hi all, > > According to the Metamath book, a comment in an *.mm file is defined as > follows (Appendix E, Metamath Language EBNF, page 213): > > _COMMENT ::= ’$(’ (_WHITECHAR+ (PRINTABLE-SEQUENCE - ’$)’)* _WHITECHAR+ > ’$)’ _WHITECHAR > > Is my understanding correct that it is not possible to have x$) inside a > comment where x is not a _WHITECHAR? For example, I cannot have such a > comment: > > $( some ($) text $) > > Also, since the combination of characters $) doesn’t have any meaning > outside of a comment, it is not possible to use x$) (where x is not a > _WHITECHAR) anywhere inside an *.mm file. Is this right? > > - > Igor > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/b9445f01-b963-41a9-a390-c34851e12717n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b9445f01-b963-41a9-a390-c34851e12717n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CADBQv9bzjijJO6OhjpvkT3eXKpUtBMUSa1GAE7tKLjRtGgDNFw%40mail.gmail.com.
