Lean4
/-- `rw??` is an interactive tactic that suggests rewrites for any expression selected by the user.
To use it, shift-click an expression in the goal or a hypothesis that you want to rewrite.
Clicking on one of the rewrite suggestions will paste the relevant rewrite tactic into the editor.
The rewrite suggestions are grouped and sorted by the pattern that the rewrite lemmas match with.
Rewrites that don't change the goal and rewrites that create the same goal as another rewrite
are filtered out, as well as rewrites that have new metavariables in the replacement expression.
To see all suggestions, click on the filter button (▼) in the top right.
-/
@[tactic_parser 1000]
public meta def tacticRw?? : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.LibraryRewrite.tacticRw?? 1024 (ParserDescr.nonReservedSymbol✝ "rw??" false✝)
