expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
11 stars 4 forks source link

Allow merging multiple statements with one merge button click #149

Closed CatsAreFluffy closed 11 months ago

CatsAreFluffy commented 11 months ago

It'd make merging lots of stuff a lot faster.

expln commented 11 months ago

What do you mean by merging? There is a button which merges two identical statements. It merges in the sense that it removes one statement and replaces all references to it with references to the remaining statement. But what kind of merging do you mean? Can you provide an example/examples?

CatsAreFluffy commented 11 months ago

Yes, I mean that kind of merging. For example, when I'm applying a theorem that uses lots of abbreviations (like many group theory theorems), after unifying the arguments I have to click many times to merge the abbreviations.

expln commented 11 months ago

Ok, got it. I've just recently implemented this feature. I will deploy it to dev tomorrow and describe how it works.

expln commented 11 months ago

This is ready on dev https://expln.github.io/lamp/dev/index.html

Now you don't have to select statements to merge. If there are duplicated statements, you may just click the Merge button once and it will go over all the duplicated statements and will ask you what statement to use (and what to remove). For example, if there are two pairs of duplicated statements, then you may click the Merge button only once when all the statements are unselected, and the merge dialog will appear twice - one time for each of the pair.

Also, please check the "Merge similar steps automatically" setting here https://github.com/expln/metamath-lamp/issues/47#issuecomment-1662886526 Enabling this setting will merge duplicated statements automatically in some cases so you don't even need to click the Merge button.

expln commented 11 months ago

This is available in version 16