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.
