tacticChoose!___Using_ — Mathlib

Lean4

@[inherit_doc choose, tactic_parser 1000]
public meta def tacticChoose!___Using_ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Choose.tacticChoose!___Using_ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "choose!" false✝)
        (ParserDescr.unary✝ `many1
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt)) Lean.binderIdent)))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.cat✝ `term 0))))

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