feat: PProd and MProd syntax (part 2) (#4730)

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.)

src/Init/NotationExtra.lean

@@ -163,7 +163,6 @@ end Lean
   | `($(_) $x $y)          => `(($x, $y))
   | _                      => throw ()
 
-/-
 @[app_unexpander PProd.mk] def unexpandPProdMk : Lean.PrettyPrinter.Unexpander
   | `($(_) $x ($y, $ys,*)ₚ) => `(($x, $y, $ys,*)ₚ)
   | `($(_) $x $y)           => `(($x, $y)ₚ)
@@ -173,7 +172,6 @@ end Lean
   | `($(_) $x ($y, $ys,*)ₘ) => `(($x, $y, $ys,*)ₘ)
   | `($(_) $x $y)           => `(($x, $y)ₘ)
   | _                       => throw ()
--/
 
 @[app_unexpander ite] def unexpandIte : Lean.PrettyPrinter.Unexpander
   | `($(_) $c $t $e) => `(if $c then $t else $e)

src/Lean/Elab/BuiltinNotation.lean

@@ -330,7 +330,6 @@ where
     return (← expandCDot? pairs).getD pairs
   | _ => Macro.throwUnsupported
 
-/-
 @[builtin_macro Lean.Parser.Term.ptuple] def expandPTuple : Macro
   | `(()ₚ) => ``(PUnit.unit)
   | `(($e, $es,*)ₚ) => mkPPairs (#[e] ++ es)
@@ -339,7 +338,6 @@ where
 @[builtin_macro Lean.Parser.Term.mtuple] def expandMTuple : Macro
   | `(($e, $es,*)ₘ) => mkMPairs (#[e] ++ es)
   | _ => Macro.throwUnsupported
--/
 
 @[builtin_macro Lean.Parser.Term.typeAscription] def expandTypeAscription : Macro
   | `(($e : $(type)?)) => do

tests/lean/run/PUnit_syntax.lean

@@ -0,0 +1,47 @@
+/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
+#guard_msgs in
+#check Bool ×ₚ Nat ×ₚ List Unit
+
+/-- info: Bool ×ₚ Nat ×ₚ List Unit : Type -/
+#guard_msgs in
+#check PProd Bool (PProd Nat (List Unit))
+
+/-- info: (Bool ×ₚ Nat) ×ₚ List Unit : Type -/
+#guard_msgs in
+#check PProd (PProd Bool Nat) (List Unit)
+
+/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
+#guard_msgs in
+#check Bool ×ₘ Nat ×ₘ List Unit
+
+/-- info: Bool ×ₘ Nat ×ₘ List Unit : Type -/
+#guard_msgs in
+#check MProd Bool (MProd Nat (List Unit))
+
+/-- info: (Bool ×ₘ Nat) ×ₘ List Unit : Type -/
+#guard_msgs in
+#check MProd (MProd Bool Nat) (List Unit)
+
+/-- info: PUnit.unit : PUnit -/
+#guard_msgs in
+#check ()ₚ
+
+/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
+#guard_msgs in
+#check (true, 5, [()])ₚ
+
+/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
+#guard_msgs in
+#check (true, 5, [()])ₘ
+
+/-- info: (true, 5, [()])ₚ : Bool ×ₚ Nat ×ₚ List Unit -/
+#guard_msgs in
+#check PProd.mk true (PProd.mk 5 [()])
+
+/-- info: (true, 5, [()])ₘ : Bool ×ₘ Nat ×ₘ List Unit -/
+#guard_msgs in
+#check MProd.mk true (MProd.mk 5 [()])
+
+/-- info: PUnit.unit.{u} : PUnit -/
+#guard_msgs in
+#check PUnit.unit