Use of parentheses for new definitions

[Ender Ting]

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.

[Matthew House]

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 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 <freelance...@gmail.com> 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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/59a18a7f-a665-402e-82ff-8d727bd67d04n%40googlegroups.com.

[Thierry Arnoux]

In the mean time I have proposed df-chn in my Mathbox, which I believe is exactly what you need: a chain in the sense of order theory.

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

To view this discussion visit https://groups.google.com/d/msgid/metamath/CADBQv9b0uCHKnYPxRDDURFtXi2sAqvPfA8bti5AsxFAJHG6U7Q%40mail.gmail.com.