def Lean.Meta.Rewrites.rewriteResultLemma (r : Meta.RewriteResult) : Option 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.

Equations

• Lean.Meta.Rewrites.forwardWeight = 2

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 : RwDirection
• backward : RwDirection

def Lean.Meta.Rewrites.localHypotheses (except : List FVarId := []) : MetaM (Array (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 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 : MetaM (LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection))

Equations

• Lean.Meta.Rewrites.createModuleTreeRef = Lean.Meta.LazyDiscrTree.createModuleTreeRef Lean.Meta.Rewrites.addImport✝ Lean.Meta.Rewrites.droppedKeys

def Lean.Meta.Rewrites.incPrio : Nat → Name × RwDirection → 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 : LazyDiscrTree.ModuleDiscrTreeRef (Name × RwDirection)) : Expr → MetaM (Array (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 : 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.

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 : SideConditions
• assumption : SideConditions
• solveByElim : SideConditions

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

Shortcut for calling solveByElim.

Equations

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

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)

Equations

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

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.

Equations

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

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

Equations

• r.newGoal = if r.rfl? = true then none else some r.result.eNew

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

Equations

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

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)

Equations

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

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.

Equations

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