Lean4
/-- Notation for vectors in Lp space. `!₂[x, y, ...]` is a shorthand for
`WithLp.toLp 2 ![x, y, ...]`, of type `EuclideanSpace _ (Fin _)`.
This also works for other subscripts. -/
@[term_parser 1000]
public meta def vecNotation : Lean.ParserDescr✝ :=
ParserDescr.node✝ `PiLp.vecNotation 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "!") (ParserDescr.const✝ `noWs))
(ParserDescr.parser✝ `Mathlib.Tactic.subscriptTerm))
(ParserDescr.const✝ `noWs))
(ParserDescr.symbol✝ "["))
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))
