tacticObserve?__:_Using__,, — Mathlib

Lean4
@[inherit_doc observe, tactic_parser 1000]
public meta def «tacticObserve?__:_Using__,,» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.LibrarySearch.«tacticObserve?__:_Using__,,» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "observe?" false✝)
              (ParserDescr.unary✝ `optional
                (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))))
            (ParserDescr.symbol✝ " : "))
          (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ " using "))
      ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝)
        (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) (ParserDescr.cat✝ `term 0)) ","
        (ParserDescr.symbol✝ ", ") Bool.false✝))
Похожие утверждения