expln/metamath-lamp

Prohibit substitutions which modify global essential statements

expln opened this issue · 0 comments

expln commented

(an improper simultaneous substitution - when a variable appears on the left and right of a rule)

When there are global essential statements (i.e. loaded from external sources) and if an improper simultaneous substitution tries to replace a variable in one or few global essential statements this may lead to errors because global essential statements are read-only, mm-lamp doesn't modify them during the global substitution.

This should be fixed by prohibiting such substitutions.