Hrm. My set.mm is just from the HEAD of master, which indeed looks old:
$ git log -1 --pretty=reference
3921b733 (last release with old axiom numbers, 2018-12-20)
Your comment prompted me to look more closely at the repo. I guess the latest
set.mm is on the `develop' branch instead?
> By the way, this definition was an experiment in my mathbox only - it has
> no offical meaning (and will never become official I think).
Thank you for pointing this out. I didn't realize I had bumped into a mathbox.
At the moment I am just perusing around set.mm to get acquainted with
definitions, conventions, and how familiar theorems and proofs are stated
formally. IIRC, I ran into ~ caov while searching around for some other syntax.
Anyway, sorry for the false alarm.
Alexander van der Vekens <[email protected]> wrote:
> 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/3FAOPDLXKGS5U.36XUAB3KEJ8DM%40wilsonb.com.
