Support for grw suggestions in #click_suggestions

structure Mathlib.Tactic.ClickSuggestions.GrwPos : Type

GRewritePos contains the ìnformation about a given subexpression position needed for applying a grw lemma.

• relName : Lean.Name

  The name of the relation.

• relation : Lean.Expr

  The expression of the relation.

• symm? : Option Bool

  symm is none if the given relations are symmetric. symm is true when you can only rewrite from right to left.

def Mathlib.Tactic.ClickSuggestions.getGrwPos? (rootExpr subExpr : Lean.Expr) (pos : Lean.SubExpr.Pos) (hyp? : Bool) : Lean.MetaM (Array GrwPos)

Determine possible ways in which a grw call could rewrite at the given subexpression.

Equations

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

structure Mathlib.Tactic.ClickSuggestions.GrwLemma : 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

• relName : Lean.Name

  relName is the relation of the lemma.

structure Mathlib.Tactic.ClickSuggestions.GrwInfo : Type

The information needed for doing a grewrite.

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

• gpos : Array GrwPos

  The relations that can be used for rewriting.

• rwKind : RwKind

  Some information about the rewrite position.

structure Mathlib.Tactic.ClickSuggestions.GrwKey : Type

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

• numGoals : ℕ

  The number of side goals created.

• nameLength : ℕ

  The name length of the used lemma.

• replacementSize : ℕ

  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.instInhabitedGrwKey : Inhabited GrwKey

Equations

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

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instOrdGrwKey : Ord GrwKey

Equations

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

def Mathlib.Tactic.ClickSuggestions.GrwKey.isDuplicate (a b : GrwKey) : 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.GrwLemma.try (i : GrwInfo) (lem : GrwLemma) : ClickSuggestionsM (Result GrwKey)

Generate the suggestion for rewriting with lem.

Equations

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