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.
