Infrastructure for searching and displaying sets of lemmas

This is used for apply, apply at, rw and grw suggestions.

structure Mathlib.Tactic.ClickSuggestions.Result (α : Type) : Type

Result stores the information from a lemma that was successfully applied.

• filtered : Option ProofWidgets.Html

  filtered will be shown in the filtered view.

• unfiltered : ProofWidgets.Html

  unfiltered will be shown in the unfiltered view.

• key : α

  key is used for sorting and comparing theorems.

• pattern : ProofWidgets.Html

  The pattern of the first lemma in a section is shown as the header of that section.

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instInhabitedResult {a✝ : Type} [Inhabited a✝] : Inhabited (Result a✝)

Equations

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

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instOrdResult {α : Type} [Ord α] : Ord (Result α)

Equations

• Mathlib.Tactic.ClickSuggestions.instOrdResult = { compare := fun (x1 x2 : Mathlib.Tactic.ClickSuggestions.Result α) => compare x1.key x2.key }

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instLTResult {α : Type} [Ord α] : LT (Result α)

Equations

• Mathlib.Tactic.ClickSuggestions.instLTResult = ltOfOrd

Maintaining the state of the widget

structure Mathlib.Tactic.ClickSuggestions.SectionState (α : Type) : Type

The state of one section of library search suggestions. We use this for 4 kinds of suggestions: rw, grw, apply and apply at.

• results : Array (Result α)

  The results of the theorems that successfully applied.

• errors : Array ProofWidgets.Html

  The results of the theorems that threw an error when trying to apply them. Usually, errors will be caught, except for when using click_suggestions.debug.

instance Mathlib.Tactic.ClickSuggestions.instNonemptySectionState {α✝ : Type} : Nonempty (SectionState α✝)

@[specialize #[]]

def Mathlib.Tactic.ClickSuggestions.Result.insertInArray {α : Type} [Ord α] [Inhabited α] (res : Result α) (arr : Array (Result α)) (isDup : α → α → Lean.MetaM Bool) : Lean.MetaM (Array (Result α))

Insert the new result res into the array arr of already existing results.

We maintain the invariants that results is sorted, and for each set of duplicate results, only the first one can have the filtered field set to some.

Equations

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

def Mathlib.Tactic.ClickSuggestions.SectionState.insertResult {α : Type} [Ord α] [Inhabited α] (s : SectionState α) (res : Result α) (isDup : α → α → Lean.MetaM Bool) : Lean.MetaM (SectionState α)

Insert res into the section state s.

Equations

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

inductive Mathlib.Tactic.ClickSuggestions.SectionKind : Type

Whether the section corresponds to local hypotheses, declarations from the current file, or imported declarations.

• hyp : SectionKind
• currFile : SectionKind
• imported : SectionKind

def Mathlib.Tactic.ClickSuggestions.renderSection {α : Type} (tactic : String) (kind : SectionKind) (s : SectionState α) : ProofWidgets.Html

Create the HTML corresponding to s.

Equations

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

@[specialize #[]]

def Mathlib.Tactic.ClickSuggestions.spawnTask {α : Type} (premise : Premise) (k : ClickSuggestionsM α) : ClickSuggestionsM (Task (Except ProofWidgets.Html (Option α)))

Spawn a task that computes a piece of Html to be displayed when finished.

Equations

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