Parsing comments in *.mm files

[Igor Ieskov]

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

[Matthew House]

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

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/b9445f01-b963-41a9-a390-c34851e12717n%40googlegroups.com.