Bookkeeping: mainly uniformize nf.mm preamble and headers with (i)set.mm #3779
Conversation
|
The second, third, and fourth commits are independent and address miu.mm, ql.mm, and demo0.mm/big-unifier.mm respectively. This finishes the work I wanted to do now regarding standardization of databases in this repo. |
There was a problem hiding this comment.
This is a good set of changes. Nice to see this.
I did find three small things (well small in terms of how much text is affected at least, I don't know whether my suggestions are controversial or not). Perhaps depending on what people think we can try to address those here or split them apart into separate pull request(s).
| $c & $. $( Ampersand (read: "and-also") $) | ||
| $c => $. $( Big-to (read: "proves") $) | ||
| $c & $. $( Ampersand (read: "and"). $) | ||
| $c => $. $( Double right arrow (read: "implies"). $) |
There was a problem hiding this comment.
I'm not a fan of "implies" here because this is not -> which would be read as implies.
Probably my preferrred solution would be to just omit the (read: "proves") text because I'm not sure people say these out loud using the suggested pronunciation.
Same comment applies to the line above and (read: "and-also")
Whatever we decide would apply to the versions of this comment in set.mm, nf.mm, and whereever else it appears as well.
There was a problem hiding this comment.
Some authors also use "entails". I think "and" is better that "and-also", and "proves" is not good. I find implies better and not too confusing. But if you think this may confuse new readers (since indeed we have "formula-level implication" ->), then maybe we can remove them altogether.
There was a problem hiding this comment.
I'd go for "remove them altogether" at least here.
There was a problem hiding this comment.
To locate it, I searched "ampersand", and ran into https://us.metamath.org/mpeuni/conventions.html where the double right arrow is also given as "implies".
There was a problem hiding this comment.
Heh. I suppose given how many words we spend on this topic both in that conventions page and sections on "deduction theorem" and so on, a single choice of word here isn't going to make or break anything. So I guess I don't feel super strongly.
Bookkeeping: mainly uniformize nf.mm preamble and headers with (i)set.mm, as well as iset.mm with set.mm, taking each time the more detailed/up-to-date version. A few corrections along the way: one contribution date, some erroneous file names.
Part of #905
Since this touches nf.mm, ping @scott-fenton @sctfn and FYI @jkingdon for iset.mm.
edit: easy review can be done by opening the (diffs of the) three files side-by-side (at least it was convenient for me, on a wide screen).