def Lean.Meta.Rewrites.rewriteResultLemma (r : Meta.RewriteResult) : Option Expr

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

def Lean.Meta.Rewrites.forwardWeight : Nat

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

def Lean.Meta.Rewrites.backwardWeight : Nat

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

inductive Lean.Meta.Rewrites.RwDirection : Type

• forward : RwDirection
• backward : RwDirection

def Lean.Meta.Rewrites.localHypotheses (except : List FVarId := []) : MetaM (Array (Expr × Bool × Nat))

Select = and ↔ local hypotheses.

def Lean.Meta.Rewrites.droppedKeys : List (List LazyDiscrTree.Key)

We drop .star and Eq * * * from the discriminator trees because they match too much.

def Lean.Meta.Rewrites.createModuleTreeRef : MetaM (LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection))

def Lean.Meta.Rewrites.incPrio : Nat → Name × RwDirection → Name × Bool × Nat

def Lean.Meta.Rewrites.rwFindDecls (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) : Expr → MetaM (Array (Name × Bool × Nat))

Create function for finding relevant declarations.

structure Lean.Meta.Rewrites.RewriteResult : Type

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

• expr : 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 : Meta.RewriteResult

  The result from the rw tactic.

• mctx : MetavarContext

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

• rfl? : Bool

def Lean.Meta.Rewrites.dischargableWithRfl? (mctx : MetavarContext) (e : Expr) : MetaM Bool

Check to see if this expression (which must be a type) can be closed by with_reducible rfl.

inductive Lean.Meta.Rewrites.SideConditions : Type

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

• none : SideConditions
• assumption : SideConditions
• solveByElim : SideConditions

def Lean.Meta.Rewrites.solveByElim (goals : List MVarId) (depth : Nat := 6) : MetaM PUnit

Shortcut for calling solveByElim.

def Lean.Meta.Rewrites.rwLemma (ctx : MetavarContext) (goal : MVarId) (target : Expr) (side : SideConditions := SideConditions.solveByElim) (lem : Expr ⊕ Name) (symm : Bool) (weight : Nat) : MetaM (Option RewriteResult)

partial def Lean.Meta.Rewrites.getSubexpressionMatches {α : Type} (op : Expr → MetaM (Array α)) (e : Expr) : MetaM (Array α)

Find keys which match the expression, or some subexpression.

Note that repeated subexpressions will be visited each time they appear, making this operation potentially very expensive. It would be good to solve this problem!

Implementation: we reverse the results from getMatch, so that we return lemmas matching larger subexpressions first, and amongst those we return more specific lemmas first.

def Lean.Meta.Rewrites.rewriteCandidates (hyps : Array (Expr × Bool × Nat)) (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) (target : Expr) (forbidden : NameSet := ∅) : MetaM (Array ((Expr ⊕ Name) × Bool × Nat))

Find lemmas which can rewrite the goal.

See also rewrites for a more convenient interface.

def Lean.Meta.Rewrites.RewriteResult.newGoal (r : RewriteResult) : Option Expr

def Lean.Meta.Rewrites.RewriteResult.addSuggestion (ref : Syntax) (r : RewriteResult) (checkState? : Option Elab.Tactic.SavedState := none) : Elab.Tactic.TacticM Unit

structure Lean.Meta.Rewrites.RewriteResultConfig : Type

• stopAtRfl : Bool
• max : Nat
• minHeartbeats : Nat
• goal : MVarId
• target : Expr
• side : SideConditions
• mctx : MetavarContext

def Lean.Meta.Rewrites.takeListAux (cfg : RewriteResultConfig) (seen : Std.HashMap String Unit) (acc : Array RewriteResult) (xs : List ((Expr ⊕ Name) × Bool × Nat)) : MetaM (Array RewriteResult)

def Lean.Meta.Rewrites.findRewrites (hyps : Array (Expr × Bool × Nat)) (moduleRef : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) (goal : MVarId) (target : Expr) (forbidden : NameSet := ∅) (side : SideConditions := SideConditions.solveByElim) (stopAtRfl : Bool) (max : Nat := 20) (leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult)

Find lemmas which can rewrite the goal.