tacticLinear_combination2____ — Mathlib

Lean4

@[inherit_doc linearCombination', tactic_parser 1000]
public meta def tacticLinear_combination2____ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.LinearCombination'.tacticLinear_combination2____ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "linear_combination2" false✝)
        (ParserDescr.unary✝ `optional Mathlib.Tactic.LinearCombination'.normStx))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
          (ParserDescr.cat✝ `term 0))))

Похожие утверждения