Support for apply suggestions in #click_suggestions

structure Mathlib.Tactic.ClickSuggestions.ApplyLemma : Type

The structure for apply lemmas stored in the RefinedDiscrTree.

• name : Premise

  The lemma

structure Mathlib.Tactic.ClickSuggestions.ApplyKey : Type

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

• numGoals : Nat

  How many new goals are generated.

• nameLength : Nat

  The name length of the used lemma.

• replacementSize : Nat

  The total length of the new goals when printed.

• name : String

  The name of the used lemma.

• newGoals : Array Lean.Meta.AbstractMVarsResult

  The new goals.

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instInhabitedApplyKey : Inhabited ApplyKey

Equations

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

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instOrdApplyKey : Ord ApplyKey

Equations

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

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

Whether the two suggestions are duplicates of each other.

Equations

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

def Mathlib.Tactic.ClickSuggestions.ApplyLemma.try (lem : ApplyLemma) : ClickSuggestionsM (Result ApplyKey)

Generate the suggestion for applying lem.

Equations

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