I'm working on implementing comment parsing in my verifier. It doesn't seem to lend itself well to elegant implementations, however, since the token structure of comments seems to be different than that of non-comment text. In addition, the token rules of $t comments and ordinary comments seems to be different (for example, normal comments don't have the C-style comments, but $t comments do).
I can certainly figure this out by handling all the special cases and bolting together a few different parsers, but I'm wondering if anyone has found an nice technique for this. - Philip -- 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 on the web visit https://groups.google.com/d/msgid/metamath/20220512184626.4b626001%40ithilien.
