Thierry Arnoux has created this big pull request here: https://github.com/david-a-wheeler/metamath-knife/pull/9 <https://github.com/david-a-wheeler/metamath-knife/pull/9> "This PR brings in the "grammar" changes discussed with Mario... It also includes a mechanism for parsing parser commands.”
I intend to merge this, but it’s a substantial change, so if someone thinks there’s a serious problem I think we’d all like to know! --- David A. Wheeler -- 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/57471B92-04B2-4F48-9BDC-D796601F58D0%40dwheeler.com.
