expStx — Mathlib

Lean4
/-- The `(exp := n)` syntax for `linear_combination` says to take the goal to the `n`th power before
subtracting the given combination of hypotheses.
-/
meta def expStx : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "expStx" `Mathlib.Tactic.LinearCombination.expStx
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.unary✝ `atomic
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " (")
              ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "exp" false✝))
            (ParserDescr.symbol✝ " := ")))
        (ParserDescr.unary✝ `withoutPosition (ParserDescr.const✝ `num)))
      (ParserDescr.symbol✝ ")"))
Похожие утверждения