renames of syl theorems

58 views
Skip to first unread message

Jim Kingdon

unread,
Nov 13, 2023, 11:40:32 PM11/13/23
to metamath
This discussion has been a bit spread across a few issues and pull
requests, so it seems good to offer a message here about the rename
underway to some of the theorems with "syl" in their names. There is a
list of all the theorems affected here:
https://github.com/metamath/set.mm/blob/develop/changes-set.txt#L35 .
I'm starting with the syl5 ones.

Because each of these pull requests (two have been merged so far) touch
a lot of lines, it probably is better to merge them quickly rather than
leave a lot of time between approval and merging, so if you see any
proposed renames in the above list which you think should be changed or
considered at more length, speak up now (here on the mailing list, make
a github issue, make a pull request to the change-set.txt file, etc).


Glauco

unread,
Nov 14, 2023, 3:34:25 AM11/14/23
to Metamath
This is going to somehow obsolete the model used by Yamma, for step suggestions.

Currently, it is built by a script (it cannot be invoked within the extension; you need the repo and a Typescript dev environment).

A solution would be to add a command to allow the extension itself to update the model, and I will work on that.
Reply all
Reply to author
Forward
0 new messages