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

In visualizations, don't repeat if conclusion is all constants (low priority) #115

Closed david-a-wheeler closed 1 year ago

david-a-wheeler commented 1 year ago

In visualizations, if the concluding justification is all constants, then the resulting statement shouldn't be repeated because it adds no new information. E.g., if you visualize df-2, you see:

---------------------
|- 2 = ( 1 + 1 )
|- 2 = ( 1 + 1 )

There's no point in showing it twice, because there are no variables to map to. Being able to show the visualization is great even in this case, because it reveals that this conclusion really is all constants... we just don't need that duplicated.

expln commented 1 year ago

@david-a-wheeler This is fixed on dev.

expln commented 1 year ago

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