feat: PProd and MProd syntax (part 2)

[nomeata]

the internal constructions for structural and well-founded recursion
use plenty of PProd and MProd, and reading these, deeply
nested and in prefix notation, is unnecessarily troublesome.

Therefore this introduces notations

a ×ₚ b   -- PProd a b
a ×ₘ b   -- MProd a b
()ₚ      -- PUnit.unit
(x,y,z)ₚ -- PProd.mk x (PProd.mk y z)
(x,y,z)ₘ -- MProd.mk x (MProd.mk y z)

(This is the post-stage0-part 2.)

[nomeata]

Not sure if it is acceptable to waste syntax space on something internal like this, hence marking as awaiting-review.

This seems to need a stage0 update after defining the parser, unless I am mistaken.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-07-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-07-12 09:34:26)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ab0241dac8204402a42f6820071561ee7bbe4801 --onto 5f70c1ca64a2c05a5866c47b9eb80a92034433ec. (2024-07-15 15:43:00)

[kmill]

Not sure if it is acceptable to waste syntax space on something internal like this, hence marking as awaiting-review.

I was just about to take a look at this PR at the start of my day and was surprised to see it's already been merged — that gave me just one working day, and Friday I wasn't doing any Lean.

I'm not sure about global "p" and "m" tuple notation. Are users supposed to figure out they mean "polymorphic" and "monomorphic"? Should these notations be scoped since these are fairly specialized? Are there alternative notations? Did we check other projects that we're not stepping on their pre-existing notations?

I would have strongly suggested that the notation PProd use ×' since PSigma already uses it, and then it would parallel the notation for Prod/Sigma, at least for types. This is missing any special notation for PProd terms however.

[nomeata]

You are absolutely right, I was a bit too trigger happy with this PR.

I disregarded ×' because it is already used for PSigma, but you are right that this is actually more reason to use it here.

And for terms: Special syntax isn’t actually needed given that we can use angle brackets.

I’ll change this tomorrow or so.

Sorry for the confusion, I should have waited for your feedback.