Support for rw suggestions in #click_suggestions

structure Mathlib.Tactic.ClickSuggestions.RwLemma : Type

The structure for rewrite lemmas stored in the RefinedDiscrTree.

• name : Premise

  The lemma

• symm : Bool

  symm is true when rewriting from right to left

structure Mathlib.Tactic.ClickSuggestions.RwInfo : Type

The information needed for doing a rewrite.

• rootExpr : Lean.Expr

  The outer expression in which the rewrite takes place.

• subExpr : Lean.Expr

  The expression that is being rewritten.

• rflTarget? : Option Lean.Expr

  If we rewrite into this expression, then the goal will be solved.

• pos : Lean.SubExpr.Pos

  The expression that is being rewritten. This may not be the same as the selected expression, because we also suggest rewriting partial applications.

• rwKind : RwKind

  Some information about the rewrite position.

structure Mathlib.Tactic.ClickSuggestions.RwKey : Type

The key that is used for sorting and deduplicating rw lemmas.

• numGoals : Nat

  The number of side goals created.

• symm : Bool

  If symm := true, then the rewrite is right-to-left.

• nameLength : Nat

  The name length of the used lemma.

• replacementSize : Nat

  The length of the new subexpression.

• name : String

  The nae of the used lemma.

• replacement : Lean.Meta.AbstractMVarsResult

  The new subexpression.

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instInhabitedRwKey : Inhabited RwKey

Equations

• Mathlib.Tactic.ClickSuggestions.instInhabitedRwKey = { default := Mathlib.Tactic.ClickSuggestions.instInhabitedRwKey.default }

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instOrdRwKey : Ord RwKey

Equations

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

def Mathlib.Tactic.ClickSuggestions.RwKey.isDuplicate (a b : RwKey) : Lean.MetaM Bool

Whether the two suggestions are duplicates of each other.

Equations

• a.isDuplicate b = (pure (a.replacement.mvars.size == b.replacement.mvars.size) <&&> Mathlib.Tactic.ClickSuggestions.isExplicitEq a.replacement.expr b.replacement.expr)

def Mathlib.Tactic.ClickSuggestions.RwLemma.try (i : RwInfo) (lem : RwLemma) : ClickSuggestionsM (Result RwKey)

Generate the suggestion for rewriting with lem.

Equations

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