Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
Yes, you may do this change. I intentionally left ...st in those places to make adding new attributes easier, but looks like new attributes will not be added (or this will happen not very soon).
The warning 23 is being suppressed. Warning 23 is: Useless record "with" clause.
I am looking into not suppressing the warning 23 and fixing the code so that the warning doesn't occur.
Are you interested in me pursuing this and submitting such changes?
The following are the three cases that arise.
A) file MM_cmp_root_stmts.res (This seems straightforward)
Change from:
to:
B) file MM_cmp_multiline_text.res
Change from:
to:
C) file MM_cmp_pe_stmt.res
Change from:
to: