propose' — Mathlib

Lean4
/-- * `have? using a, b, c` tries to find a lemma
  which makes use of each of the local hypotheses `a, b, c`,
  and reports any results via trace messages.
* `have? : h using a, b, c` only returns lemmas whose type matches `h` (which may contain `_`).
* `have?! using a, b, c` will also call `have` to add results to the local goal state.

Note that `have?` (unlike `apply?`) does not inspect the goal at all,
only the types of the lemmas in the `using` clause.

`have?` should not be left in proofs; it is a search tool, like `apply?`.

Suggestions are printed as `have := f a b c`.
-/
@[tactic_parser 1000]
public meta def propose' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.Propose.propose' 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "have?" false✝)
              (ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
            (ParserDescr.unary✝ `optional (ParserDescr.const✝ `ident)))
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `andthen (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✝))
Похожие утверждения