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

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

Equations

• Lean.Meta.Rewrites.rewriteResultLemma r = if r.eqProof.isAppOfArity `congrArg 6 = true then some (r.eqProof.getArg! 5) else none

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.

Equations

• Lean.Meta.Rewrites.backwardWeight = 1

inductive Lean.Meta.Rewrites.RwDirection : Type

• forward: Lean.Meta.Rewrites.RwDirection
• backward: Lean.Meta.Rewrites.RwDirection

def Lean.Meta.Rewrites.localHypotheses (except : 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 Lean.Meta.Rewrites.droppedKeys : List (List Lean.Meta.LazyDiscrTree.Key)

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

Equations

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

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

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

Equations

• Lean.Meta.Rewrites.incPrio x (nm, Lean.Meta.Rewrites.RwDirection.forward) = (nm, false, 2 * x)
• Lean.Meta.Rewrites.incPrio x (nm, Lean.Meta.Rewrites.RwDirection.backward) = (nm, true, x)

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

Create function for finding relevant declarations.

Equations

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

structure Lean.Meta.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.

• 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.

• rfl? : Bool

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

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

Equations

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

inductive Lean.Meta.Rewrites.SideConditions : Type

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

• none: Lean.Meta.Rewrites.SideConditions
• assumption: Lean.Meta.Rewrites.SideConditions
• solveByElim: Lean.Meta.Rewrites.SideConditions

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

Shortcut for calling solveByElim.

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

Equations

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

partial def Lean.Meta.Rewrites.getSubexpressionMatches {α : Type} (op : Lean.Expr → Lean.MetaM (Array α)) (e : Lean.Expr) : Lean.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 (Lean.Expr × Bool × Nat)) (moduleRef : Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef (Lean.Name × Lean.Meta.Rewrites.RwDirection)) (target : Lean.Expr) (forbidden : Lean.NameSet := ∅) : Lean.MetaM (Array ((Lean.Expr ⊕ Lean.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 : Lean.Meta.Rewrites.RewriteResult) : Option Lean.Expr

Equations

• r.newGoal = if r.rfl? = true then some (Lean.Expr.lit (Lean.Literal.strVal "no goals")) else some r.result.eNew

def Lean.Meta.Rewrites.RewriteResult.addSuggestion (ref : Lean.Syntax) (r : Lean.Meta.Rewrites.RewriteResult) : Lean.Elab.TermElabM Unit

structure Lean.Meta.Rewrites.RewriteResultConfig : Type

• stopAtRfl : Bool
• max : Nat
• minHeartbeats : Nat
• goal : Lean.MVarId
• target : Lean.Expr
• side : Lean.Meta.Rewrites.SideConditions
• mctx : Lean.MetavarContext

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

Equations

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

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

Find lemmas which can rewrite the goal.