Looking at the current version of set.mm, the comment of the definition
caov is
$( 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 a pair of
parentheses in
contrast to the current definition, see ~ df-ov . $)
caov $a class (( A F B )) $.
The same on the current web page http://us.metamath.org/mpeuni/caov.html.
In both versions, the comment is correct.
Where is your snippet coming from? This seems to be a very old version...
By the way, this definition was an experiment in my mathbox only - it has
no offical meaning (and will never become official I think).
Alexander
On Monday, June 22, 2020 at 2:57:04 PM UTC+2, [email protected] wrote:
>
> 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/faf5bc34-a26f-4083-b132-cc9344c56679o%40googlegroups.com.
