Typo in comment to ~ caov?

[heiph...@wilsonb.com]

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?

[Alexander van der Vekens]

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

[heiph...@wilsonb.com]

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]

There was alrady a discussion about develop/master branches: https://groups.google.com/d/topic/metamath/wM1eAAy6lb4/discussion

I can't remember the decision made there (about the usage of the master branch).

[Antony Bartlett]

The best branch for Metamath beginners to be looking at is 'develop'.  For most other projects the best branch for beginners to be looking at is 'master'.  Therefore, and speaking as a beginner myself who has already made this mistake, the only way to stop beginners being drawn to 'master' like moths to a flame is to do whatever 'master' is being used for in a branch with a different name.  David was considering renaming 'develop' to 'master' but he was afraid it would break everyone's workflow.  Perhaps there are alternatives that could be considered?  The first thing that occurs to me would be to leave a stub behind in 'master' recommending 'develop' and explaining that it is extremely stable (in the sense that proof-checkers automatically guard its correctness).

On Tue, Jun 23, 2020 at 8:21 PM 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

There was alrady a discussion about develop/master branches: https://groups.google.com/d/topic/metamath/wM1eAAy6lb4/discussion

I can't remember the decision made there (about the usage of the master branch).

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/fe21cd6c-95e1-4447-bb20-3c9774487491o%40googlegroups.com.

[heiph...@wilsonb.com]

Alexander van der Vekens <ave...@yahoo.de> wrote:

Thank you for the reference.

For posterity in case some future metamathematician stumbles across this post,
it looks like the 'develop' branch is (at this point in time) where pretty much
everyone pushes database updates, whereas 'master' only receives infrequent
updates by Norm to keep it "semi-static" for tool testing, etc.

[Dirk-Anton Broersen]

In an effort to try to “construct” the cuberoot of 2 this might be an example of at least a geometric “result”.

 

Because of the fact that, oke it’s all correct and X = ³V2, still X seems to be needed as an input rather that a result. Though it can’t be diffirent than X = ³V2

 

With friendly regards,

 

Dirk-Anton Broersen

 

 

 

 

 

 

 

 

failure: where x = not  ³V2

it does get close.