Automate creating of labels for hypotheses

[expln]

It happens very often that I get an error related to labels when adding new hypotheses. This is due to more strict rules for hypothesis labels. This should be automated to reduce necessity for a user to modify hypothesis labels manually. If possible, respecting set.mm naming convention.

[david-a-wheeler]

If the tool knew which statement was the "Goal" (e.g., my "statement type G" idea), then when a statement is converted to a hypothesis and it has a digits-only id, its id could be automatically changed to be Goal statement name + "." + smallest positive integer that produces a name not currently used. That would follow the set.mm conventions and makes a reasonable default.

[expln]

Great, this makes G-statements useful twice.

[david-a-wheeler]

I agree. In retrospect, it's reasonable that a proof assistant can provide better defaults if it knows what the current goal is :-).

[expln]

@david-a-wheeler This is implemented on dev. For steps with numeric labels, when you change P step type to H then:

• if there is a G step, then the new label will be G step name + . + int
• if there is no G step, then mm-lamp checks if the currently assigned label is valid. If it is valid, then nothing is changed. If it is invalid then another numeric valid label is generated.

So, with the latest update when you change P to H you should not see errors due to invalid labels.

[expln]

This is available in version 15 https://expln.github.io/lamp/v15/index.html