Typos in definitions for set Theory (section 3.4.3)

[avekens]

• page 78, df-clel: ") $.?" => ") $."
• page 81: df-opab: "y >. / ph ) } $" => "y >. /\ ph ) } $"
• page 83, df-fun: " Rel A / A. x " => " Rel A /\ A. x "
• page 84, df-fo: " F Fn A / ran F = B " => " F Fn A /\ ran F = B "
• page 84, df-f1o: " F : A -1-1-> B? " => " F : A -1-1-> B "

Some editorial remarks about this section:

• The names of the defined concepts should be written in bold. Especially the first definition (on page 77) comes very unexpectedly and confuses the reader after reading the preceding paragraph "The definitions we present..." - The following "Define the abstraction class." seems to be incomplete until you notice that this is the first definition presented. If it was written "Define the abstraction class.", it would be much clearer that this is the first definition.
• superfluous empty line between df-cleq.1 and df-cleq (ASCII version) on page 78?
• the line breaks for the definitions should be placed more carefully, e.g. for df-opab (ASCII version) on page 81, the line should not be broken between "E. y ( z = <." and "x, y >.", but between "E. y" and "( z = <. x, y >." or at least between "E. y ( z = " and "<. x, y >.".

[benjub]

More generally, on pages 75--84 (and maybe at other places too), it is not necessary to display the ASCII versions of the statements right after the "pretty printed" versions.

As for defined terms in boldface, I agree. Personally, I have a macro

\newcommand*{\define}[1]{\textbf{#1}}%defined terms are in bold

in most of my TeX files.

[david-a-wheeler]

Displaying the ASCII versions is certainly not necessary, and it's a lot easier to not have both. That said, having the both present was intentional, so that new readers could see "what you'll actually see when editing" instead of just the pretty final forms.

It'd be great to get input from others on whether or not to drop it.

[benjub]

Ok. Let's hear from others. There is also the intermediate option to display both the ASCII and the pretty-print only for the first or first few statements.

[avekens]

In my opinion it is very impressive to have both versions one after the other. It illustrates how logical formulas are translated into the Metamath language. Furthermore, both versions were already provided in the original version of the Metamath book, and to leave it as it is would be in the spirit of Norm's thinking.