Formal grammar

[benjub]

In Appendix E (EBNF grammar), an include-stmt can only appear in the outermost-scope-stmt. However, metamath.c v0.198 does accept include-stmts within blocks. This makes things context-dependent since an inclusion statement simply "pastes" the content of the included file at that point: since constant-stmts can only appear in the outermost-scope-stmt, the included file, if not in the outermost scope, cannot contain any constant-stmt.

So one can modify the EBNF grammar to remove include-stmt from the production rule outermost-scope-stmt ::= ... and put it instead in the production rule stmt ::= ..., but then more constraints for database validity do not appear in the grammar (since they are context-dependent). Or one can modify metamath.c to reject inclusion statements not in the outermost scope, but I think this is a non-necessary restriction. A third possibility is to accept both inclusion statements and $c statements anywhere (this is backward compatible: a database conforming to the former version also conforms to the new). I haven't thought this through, but wanted to record it here for future reference.