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.
