Lean4
/-- The command `name_poly_vars` names variables in
`MvPolynomial (Fin n) R` for the appropriate value of `n`.
The notation introduced by this command is local.
Usage:
```lean
variable (R : Type) [CommRing R]
name_poly_vars X, Y, Z over R
#check Y -- Y : MvPolynomial (Fin 3) R
```
-/
@[command_parser 1000]
public meta def namePolyVarsOver : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.namePolyVarsOver 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "name_poly_vars ")
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.const✝ `ident) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ " over "))
(ParserDescr.cat✝ `term 0))
