To Thierry: it [~df-chn] is what I need, indeed! Amazing coincidence. I'd then
- move your chain definition to main, somewhere between "5.7 Words over a set" and "17.3.1 Walks" (in "GRAPH THEORY" part) so probably to a new section "9.7 Chains" (in "BASIC ORDER THEORY" part) *Note: there is something in your htmldef that makes it render "( < Chain𝐴)" with a missing space* ; - move your chain theorems to main too; - remove ~cupword, ~df-upword which are my definitions for the same; - port those of my 'UpWord' (chain) theorems which are not obsolete, to main; - add a few equality and subset theorems to that same section in main. Is that a valid way to move forward? Additionally, when proving subsequent theorems, would I place them in my mathbox or in that section? To Matthew and to David: sounds reasonable! I'll probably stick to surrounding newly defined classes with parens if they need any arguments. Best wishes, Ender четверг, 15 января 2026 г. в 20:15:36 UTC+3, Thierry Arnoux: > In the mean time I have proposed df-chn > <https://us.metamath.org/mpeuni/df-chn.html> in my Mathbox, which I > believe is exactly what you need: a chain in the sense of order theory > <https://en.wikipedia.org/wiki/Total_order#Chains>. > > > If there was to be a rule, I'd say parentheses are used for classes, and > left away for wffs. > > For example: `( A + B )` (df-ov) is a class and has parentheses, while `A > < B` is a (df-br) is a wff and does not. > > Same for example for df-fv, df-dif, df-un, df-in (classes, parentheses), > and df-clel, df-ne, df-ss, df-po, (wff, no parentheses), etc. > > BR, > _ > Thierry > > > On 15/01/2026 17:27, Matthew House wrote: > > metamath-knife -g is pretty helpful for testing the grammar for > ambiguities. In this case, it has no complaints if I add $c AdjRelWord $. > cadjrelword $a class AdjRelWord S R $. to set.mm, so it's presumably > fine. And as you mention, its syntax is analogous to cdc > <https://us.metamath.org/mpeuni/cdc.html> in any case. > > (Though conventionally, when I see "class functions" in main set.mm > taking multiple arguments, they're written with full ( , ) particles, > e.g., if ( ph , A , B ); Pred ( R , A , X ); frecs ( R , A , F ); wrecs ( > R , A , F ); rec ( F , I ); seqom ( F , I ); sup ( A , B , R ); inf ( A , > B , R ); and OrdIso ( R , A ). Odd ones include seq M ( .+ , F ) and seq_s > M ( .+ , F ).) > > On Thu, Jan 15, 2026 at 7:43 AM Ender Ting <[email protected]> wrote: > >> I'm considering to generalize my definition UpWord S (for strictly >> increasing words on alphabet S) to AdjRelWord S R (which would have R >> instead of hard-coded <, and so could be used on other partial orders). >> >> I do not quite get if I need to put parentheses like ( AdjRelWord S R ); >> the decimal constructor ~cdc has none, the sum syntax ~csu has nothing >> between its two classes too, while ~cpred wraps its arguments in >> parentheses. In theory, the classes should already be unambiguously >> decodable as a prefix code, but I am not certain. >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion visit >> https://groups.google.com/d/msgid/metamath/59a18a7f-a665-402e-82ff-8d727bd67d04n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/59a18a7f-a665-402e-82ff-8d727bd67d04n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > > To view this discussion visit > https://groups.google.com/d/msgid/metamath/CADBQv9b0uCHKnYPxRDDURFtXi2sAqvPfA8bti5AsxFAJHG6U7Q%40mail.gmail.com > > <https://groups.google.com/d/msgid/metamath/CADBQv9b0uCHKnYPxRDDURFtXi2sAqvPfA8bti5AsxFAJHG6U7Q%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/31a87eb1-2971-4322-b026-4415307a20b6n%40googlegroups.com.
