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.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

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.

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.

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.

@[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.