observe — Mathlib

Lean4
/-- `observe hp : p` asserts the proposition `p`, and tries to prove it using `exact?`.
If no proof is found, the tactic fails.
In other words, this tactic is equivalent to `have hp : p := by exact?`.

If `hp` is omitted, then the placeholder `this` is used.

The variant `observe? hp : p` will emit a trace message of the form `have hp : p := proof_term`.
This may be particularly useful to speed up proofs. -/
@[tactic_parser 1000]
public meta def observe : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.LibrarySearch.observe 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "observe" false✝)
              (ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "?")))
            (ParserDescr.unary✝ `optional
              (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))))
          (ParserDescr.symbol✝ " : "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ")
          ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝)
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `colGt) (ParserDescr.cat✝ `term 0)) ","
            (ParserDescr.symbol✝ ", ") Bool.false✝))))
Похожие утверждения