-
Notifications
You must be signed in to change notification settings - Fork 18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Label changes #238
Comments
This is a very important issue, because with the theorem currently labeld with ~trud (formerly ~a1tru), the instruction how to convert a theorem in deduction form into a theorem in inference form (see section 3.9.3) is completely misleading. I added already a corresponding footnote in the German translation of the book. Maybe an example would be helpful here (e.g., ~hadbi123i or ~abeq2i) - although we would get additional hardcoded label names which might be changed, this would give at least more clues where to find additional material. |
Can we mark all set.mm labels in the book with a TeX macro? That way we can scrape it in CI and double check that they all exist. |
|
Since labels in
set.mm
are sometimes modified, we need to keep the book up-to-date with theses changes. They can be found in the file https://github.com/metamath/set.mm/blob/develop/changes-set.txtThe latest one which appears in the book is:
trud
-->mptru
The text was updated successfully, but these errors were encountered: