aesop_graph — Mathlib

Lean4
/-- A variant of the `aesop` tactic for use in the graph library. Changes relative
to standard `aesop`:

- We use the `SimpleGraph` rule set in addition to the default rule sets.
- We instruct Aesop's `intro` rule to unfold with `default` transparency.
- We instruct Aesop to fail if it can't fully solve the goal. This allows us to
  use `aesop_graph` for auto-params.
-/
@[tactic_parser 1000]
public meta def aesop_graph : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `aesop_graph 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "aesop_graph" false✝)
      (ParserDescr.unary✝ `many (ParserDescr.cat✝ `Aesop.tactic_clause 0)))
Похожие утверждения