This is quite trivial, but is the comment to ~ caov correct?
"Extend class notation to include the value of an operation ` F ` (such as
` + ` ) for two arguments ` A ` and ` B ` . Note that the syntax is
simply three class symbols in a row surrounded by special parentheses
(exclamation mark with underscore) in contrast to the current definition,
see ~ df-ov ."
118064 caov $a class (( A F B )) $.In particular, I am looking at the part "(exclamation mark with underscore)". Is this some historical relic, or am I just missing something obvious? -- 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 on the web visit https://groups.google.com/d/msgid/metamath/2N0JJA4NDFGYH.1YL7TURS6EINB%40wilsonb.com.
signature.asc
Description: PGP signature
