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 <http://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
<http://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/1e446fb9-e282-4d25-b85e-7e976bdbb05b%40gmx.net.
