search

metamath / set.mm

Metamath source file for logic and set theory
Other
246 stars 88 forks source link

n-ary functions (2) #4034

Closed avekens closed 4 months ago

avekens commented 4 months ago

continuation of #3997:

.

david-a-wheeler commented 4 months ago

What do you think about the -aryF idea (above)?

icecream17 commented 4 months ago

(if you're asking me, it's a great idea)

avekens commented 4 months ago

It's actually an interesting idea to call the class -aryF, so that we will have ( N-aryF X ) for N-ary endofunctions over X. I wonder, however, if I have to rewrite all proofs manually, or if there is an automatism which does (most of) the work. Meanwhile, I propose to leave the definition unchanged for the moment (and to merge this PR), and to open an issue for the change of the symbol.

tirix commented 4 months ago

Globally replacing the math token NaryF by -aryF using any text editor should basically do the trick.

avekens commented 4 months ago

Globally replacing the math token NaryF by -aryF using any text editor should basically do the trick.

but we have to switch the operands: ( X NaryF N ) => ( N -aryF X ).

tirix commented 4 months ago

Oh yes, you're right, it's not that trivial. No problem for me to merge as-is, I already approved.

avekens commented 4 months ago

Since issue #4035 is opened for changing the symbol and order of operands, this PR can be merged now.

david-a-wheeler commented 4 months ago

I'm late to the party, but yes, glad it's merged. We can discuss swapping the order in https://github.com/metamath/set.mm/issues/4035

avekens commented 3 months ago

The new HTML representation of nary functions really looks nice: (1-aryF 𝑋)
I wonder, however, if somebody gets confused and asks where the symbols 0-aryF, 1-aryF, 2-aryF and N-aryF are defined (and what the meaning of ( C X ) would be)...

icecream17 commented 3 months ago

I guess a comment could be added to df-naryf explaining that unlike most operators, the display for -aryF only has a space on the right hand side. Internally it is still ~ co , i.e. three classes in a row surrounded by parentheses