simpsProj — Mathlib

Lean4
/-- Syntax for `initialize_simps_projections`. -/
meta def simpsProj : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "simpsProj" `Lean.Parser.Command.simpsProj
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " (")
            ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) Lean.Parser.Command.simpsRule ","
              (ParserDescr.symbol✝ ", ") Bool.false✝))
          (ParserDescr.symbol✝ ")"))))
Похожие утверждения