The rewrites tactic.

rw? tries to find a lemma which can rewrite the goal.

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

Suggestions are printed as rw [h] or rw [← h].

def Lean.Meta.RewriteResult.by? (r : Lean.Meta.RewriteResult) : Option Lean.Expr

Extract the lemma, with arguments, that was used to produce a RewriteResult.

Equations

• Lean.Meta.RewriteResult.by? r = if Lean.Expr.isAppOfArity r.eqProof `Eq.ndrec 6 = true then some (Lean.Expr.getArg! r.eqProof 5 (Lean.Expr.getAppNumArgs r.eqProof)) else none

def Mathlib.Tactic.Rewrites.forwardWeight : Nat

Weight to multiply the "specificity" of a rewrite lemma by when rewriting forwards.

Equations

• Mathlib.Tactic.Rewrites.forwardWeight = 2

def Mathlib.Tactic.Rewrites.backwardWeight : Nat

Weight to multiply the "specificity" of a rewrite lemma by when rewriting backwards.

Equations

• Mathlib.Tactic.Rewrites.backwardWeight = 1

def Mathlib.Tactic.Rewrites.discrTreeConfig : Lean.Meta.WhnfCoreConfig

Configuration for DiscrTree.

Equations

• Mathlib.Tactic.Rewrites.discrTreeConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }

def Mathlib.Tactic.Rewrites.processLemma (name : Lean.Name) (constInfo : Lean.ConstantInfo) : Lean.MetaM (Array (Array Lean.Meta.DiscrTree.Key × Lean.Name × Bool × Nat))

Prepare the discrimination tree entries for a lemma.

Equations

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

def Mathlib.Tactic.Rewrites.localHypotheses (except : optParam (List Lean.FVarId) []) : Lean.MetaM (Array (Lean.Expr × Bool × Nat))

Select = and ↔ local hypotheses.

Equations

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

def Mathlib.Tactic.Rewrites.buildDiscrTree : IO (Std.Tactic.DiscrTreeCache (Lean.Name × Bool × Nat))

Construct the discrimination tree of all lemmas.

Equations

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

def Mathlib.Tactic.Rewrites.cachePath : IO System.FilePath

Equations

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

opaque Mathlib.Tactic.Rewrites.rewriteLemmas : Std.Tactic.DiscrTreeCache (Lean.Name × Bool × Nat)

Retrieve the current cache of lemmas.

structure Mathlib.Tactic.Rewrites.RewriteResult : Type

Data structure recording a potential rewrite to report from the rw? tactic.

• expr : Lean.Expr

  The lemma we rewrote by. This is Expr, not just a Name, as it may be a local hypothesis.

• symm : Bool

  True if we rewrote backwards (i.e. with rw [← h]).

• weight : Nat

  The "weight" of the rewrite. This is calculated based on how specific the rewrite rule was.

• result : Lean.Meta.RewriteResult

  The result from the rw tactic.

• ppResult? : Option String

  Pretty-printed result.

• rfl? : Option Bool

  Can the new goal in result be closed by with_reducible rfl?

• mctx : Lean.MetavarContext

  The metavariable context after the rewrite. This needs to be stored as part of the result so we can backtrack the state.

def Mathlib.Tactic.Rewrites.RewriteResult.computeRfl (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Update a RewriteResult by filling in the rfl? field if it is currently none, to reflect whether the remaining goal can be closed by with_reducible rfl.

Equations

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

def Mathlib.Tactic.Rewrites.RewriteResult.prepare_ppResult (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Pretty print the result of the rewrite, and store it for later use.

Equations

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

def Mathlib.Tactic.Rewrites.RewriteResult.ppResult (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM String

Pretty print the result of the rewrite. If this will be done more than once you should use prepare_ppResult

Equations

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

def Mathlib.Tactic.Rewrites.solveByElim (goals : List Lean.MVarId) (depth : optParam Nat 6) : Lean.MetaM PUnit.{1}

Shortcut for calling solveByElim.

Equations

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

inductive Mathlib.Tactic.Rewrites.SideConditions : Type

Should we try discharging side conditions? If so, using assumption, or solve_by_elim?

• none: Mathlib.Tactic.Rewrites.SideConditions
• assumption: Mathlib.Tactic.Rewrites.SideConditions
• solveByElim: Mathlib.Tactic.Rewrites.SideConditions

def Mathlib.Tactic.Rewrites.rewritesCore (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat)) (ctx : Lean.MetavarContext) (goal : Lean.MVarId) (target : Lean.Expr) (forbidden : optParam Lean.NameSet ∅) (side : optParam Mathlib.Tactic.Rewrites.SideConditions Mathlib.Tactic.Rewrites.SideConditions.solveByElim) : MLList Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Find lemmas which can rewrite the goal.

This core function returns a monadic list, to allow the caller to decide how long to search. See also rewrites for a more convenient interface.

Equations

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

def Mathlib.Tactic.Rewrites.rewritesDedup (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat)) (mctx : Lean.MetavarContext) (goal : Lean.MVarId) (target : Lean.Expr) (forbidden : optParam Lean.NameSet ∅) (side : optParam Mathlib.Tactic.Rewrites.SideConditions Mathlib.Tactic.Rewrites.SideConditions.solveByElim) : MLList Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Find lemmas which can rewrite the goal, and deduplicate based on pretty-printed results. Note that this builds a HashMap containing the results, and so may consume significant memory.

Equations

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

def Mathlib.Tactic.Rewrites.rewrites (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat)) (goal : Lean.MVarId) (target : Lean.Expr) (forbidden : optParam Lean.NameSet ∅) (side : optParam Mathlib.Tactic.Rewrites.SideConditions Mathlib.Tactic.Rewrites.SideConditions.solveByElim) (stopAtRfl : optParam Bool false) (max : optParam Nat 20) (leavePercentHeartbeats : optParam Nat 10) : Lean.MetaM (List Mathlib.Tactic.Rewrites.RewriteResult)

Find lemmas which can rewrite the goal.

Equations

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

def Mathlib.Tactic.Rewrites.forbidden : Lean.ParserDescr

Syntax for excluding some names, e.g. [-my_lemma, -my_theorem].

Equations

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

def Mathlib.Tactic.Rewrites.rewrites' : Lean.ParserDescr

rw? tries to find a lemma which can rewrite the goal.

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

Suggestions are printed as rw [h] or rw [← h].

You can use rw? [-my_lemma, -my_theorem] to prevent rw? using the named lemmas.

Equations

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