# The `erw?` tactic #

`erw? [r, ...]` calls `erw [r, ...]` (at hypothesis `h` if written `erw [r, ...] at h`), and then attempts to identify any subexpression which would block the use of `rw` instead. It does so by identifying subexpressions which are defeq, but not at reducible transparency.

source
opaque Mathlib.Tactic.Erw?.tactic.erw?.verbose :
Lean.Option Bool

If set to `true`, `erw?` will log more information as it attempts to identify subexpressions which would block the use of `rw` instead.

source
def Mathlib.Tactic.Erw?.erw? :
Lean.ParserDescr

`erw? [r, ...]` calls `erw [r, ...]` (at hypothesis `h` if written `erw [r, ...] at h`), and then attempts to identify any subexpression which would block the use of `rw` instead. It does so by identifying subexpressions which are defeq, but not at reducible transparency.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Erw?.logDiffs (tk : Lean.Syntax) (e₁ e₂ : Lean.Expr) :
StateT (Array (Unit → Lean.MessageData)) Lean.MetaM Bool

Check if two expressions are different at reducible transparency. Attempt to log an info message for the first subexpressions which are different (but agree at default transparency).

Also returns an array of messages for the `verbose` report.

Instances For

source
def Mathlib.Tactic.Erw?.extractRewriteEq (e : Lean.Expr) :
Lean.MetaM (Lean.Expr × Lean.Expr)

Checks that the input `Expr` represents a proof produced by `(e)rw` and returns the types of the LHS of the equality being written (one from the target, the other from the lemma used). These will be defeq, but not necessarily reducibly so.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.Erw?.extractRewriteHypEq (e : Lean.Expr) :
Lean.MetaM Lean.Expr

Checks that the input `Expr` represents a proof produced by `(e)rw at` and returns the type of the LHS of the equality (from the lemma used). This will be defeq to the hypothesis being written, but not necessarily reducibly so.

Equations

- One or more equations did not get rendered due to their size.

Instances For