normStx — Mathlib

Lean4
/-- The `(norm := $tac)` syntax says to use `tac` as a normalization postprocessor for
`linear_combination'`. The default normalizer is `ring1`, but you can override it with `ring_nf`
to get subgoals from `linear_combination'` or with `skip` to disable normalization.
-/
meta def normStx : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "normStx" `Mathlib.Tactic.LinearCombination'.normStx
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.unary✝ `atomic
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " (")
              ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "norm" false✝))
            (ParserDescr.symbol✝ " := ")))
        (ParserDescr.unary✝ `withoutPosition (ParserDescr.cat✝ `tactic 0)))
      (ParserDescr.symbol✝ ")"))
Похожие утверждения