search

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
12 stars 5 forks source link

Goal duplication puts step at end and also has type goal #107

Closed david-a-wheeler closed 1 year ago

david-a-wheeler commented 1 year ago

I selected the goal statement and clicked on "duplicate".

I expected it to create a new statement of type "P" (since there should be only 1 goal) and for the new statement to be just above the goal (since the goal should always be at the end if that setting is enabled, which it is).

In practice it added a second goal statement after the goal statement.

expln commented 1 year ago

Thanks for reporting this. I will include a fix to v11.

david-a-wheeler commented 1 year ago

No problem! It may be as simple as turning off the "goal" flag on a duplicate.

expln commented 1 year ago

You are right. The fix was that simple. It has been deployed to dev. I am closing this issue because it is relevant only for dev, and it is fixed on dev and works exactly as described. Please fill free to reopen this issue if not everything is fixed.

david-a-wheeler commented 1 year ago

Sounds great!

I found this in the process of updating the guide, so I'll update the guide to match.

I don't know of any other issues that prevent a v11 release. I would love to see undo/redo and full unification (high priority for me), but I think you should not delay v11 for those. What you have is already awesome.

FYI: I demoed v11 to my daughter, who isn't normally very interested in math, but she found the visualizations intriguing and started asking questions. They really are a big help in explaining what's going on.