For goal labels, apply same strict label validation rules as for hypotheses

[expln]

Both hypothesis and goal labels may eventually appear in an MM database. Therefore those labels are restricted by some special rules (it is described in the Metamath book, on the page 114: Each label token must be unique, and no label token may match any math symbol token). But currently mm-lamp applies such validation only to hypotheses. It should apply same validation to the goal label too.

[david-a-wheeler]

Fyu, I've created a modification to the guide to clearly note this requirement.

[david-a-wheeler]

Please only enforce this for the "context currently in use" (including current scopes). It's really helpful to be able to "recreate" existing proofs, and that won't work if this is enforced in the database region that's not in scope.

[expln]

Sure. Everything in mm-lamp works for the "context currently in use".

[expln]

This is ready on dev. The same strict rules apply to the goal statement as for the hypotheses. But there is one exception - the goal statement may be named as one of existing assertions. Otherwise there would be problems with loading existing proofs.

[david-a-wheeler]

Awesome! I was at a family reunion & other family things this weekend, so I haven't updated the docs yet, but I definitely plan to get on it.

[expln]

This is available in version 16