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

Rename icon "substitution" to "replacement" in UI. Fixes #75 #102

Closed david-a-wheeler closed 1 year ago

david-a-wheeler commented 1 year ago

The word "substitution" is confusing, because it has multiple meanings. Is it the fundamental Metamath operation? The "A with arrow" icon?

This commit changes the UI so that the "A with arrow" icon is always described as "replacement", never as "substitution". This action already used the term "replacement" in some places (e.g., "Replace with?"), but not in others. Thus, it made sense to switch this icon so it consistently uses the term replacement.

This commit does not try to rename anything in the code itself. The user doesn't care what the code calls it. The code could be changed later to match this UI naming convention, but there's no urgent need to do that.

david-a-wheeler commented 1 year ago

This fixes #75.

david-a-wheeler commented 1 year ago

@expln -will you be merging this for v11? I want the guide to match.

expln commented 1 year ago

@david-a-wheeler Sorry, I didn't have time to re-read the "Metamath's Formal System" part of the Metamath book. Without that I cannot be sure how correct this change is. But I will re-read it soon.