simpOnly_=>__ — Mathlib

Lean4
/-- * `#simp => e` runs `simp` on the expression `e` and displays the resulting expression after
  simplification.
* `#simp only [lems] => e` runs `simp only [lems]` on `e`.
* The `=>` is optional, so `#simp e` and `#simp only [lems] e` have the same behavior.
  It is mostly useful for disambiguating the expression `e` from the lemmas.
-/
@[command_parser 1000]
public meta def «command#simpOnly_=>__» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Conv.«command#simpOnly_=>__» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#simp")
              (ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
            (ParserDescr.unary✝ `optional Lean.Parser.Tactic.simpArgs))
          (ParserDescr.unary✝ `optional (ParserDescr.symbol✝ " =>")))
        (ParserDescr.const✝ `ppSpace))
      (ParserDescr.cat✝ `term 0))
Похожие утверждения