Various utilities used in #click_suggestions

def Mathlib.Tactic.ClickSuggestions.exprToHtml (e : Lean.Expr) : Lean.MetaM ProofWidgets.Html

Turn an Expr into an HTML with hover info.

def Mathlib.Tactic.ClickSuggestions.constToHtml (n : Lean.Name) : Lean.MetaM ProofWidgets.Html

Turn a constant into an HTML with hover info. This avoids the @ that may appear when using exprToHtml.

def Mathlib.Tactic.ClickSuggestions.formatToHtmlWithDoc (fmt : Std.Format) (n : Lean.Name) : Lean.MetaM ProofWidgets.Html

Display fmt with a docstring as if it is the constant n.

def Mathlib.Tactic.ClickSuggestions.tacticToHtml (tac : Lean.TSyntax `tactic) : Lean.MetaM ProofWidgets.Html

Pretty print a tactic with its docstring as hover info.

I would love to print tac with another colour, e.g. the keyword highlighting used by the editor, but I have no idea how to do this.

opaque Mathlib.Tactic.ClickSuggestions.click_suggestions.debug : Lean.Option Bool

Let #click_suggestions show the candidate lemmas that failed to apply.

inductive Mathlib.Tactic.ClickSuggestions.Premise : Type

A global constant or a free variable. Library search can return either.

• const (declName : Lean.Name) : Premise

  A global constant.

• fvar (fvarId : Lean.FVarId) : Premise

  A free variable.

@[instance_reducible]

instance Mathlib.Tactic.ClickSuggestions.instInhabitedPremise : Inhabited Premise

def Mathlib.Tactic.ClickSuggestions.Premise.toString : Premise → String

Print a premise as a string.

def Mathlib.Tactic.ClickSuggestions.Premise.length (premise : Premise) : Nat

The name length of a premise.

def Mathlib.Tactic.ClickSuggestions.Premise.getType : Premise → Lean.MetaM Lean.Expr

Get the type of a premise.

def Mathlib.Tactic.ClickSuggestions.Premise.forallMetaTelescopeReducing : Premise → Lean.MetaM (Lean.Expr × Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

Fill the premise in with fresh universe and expression metavariables.

def Mathlib.Tactic.ClickSuggestions.Premise.unresolveName : Premise → Lean.MetaM Lean.Name

Return the user-facing name of the premise, relative to the current namespace.

def Mathlib.Tactic.ClickSuggestions.Premise.toMessageData : Premise → Lean.MessageData

Print a premise using message data.

def Mathlib.Tactic.ClickSuggestions.Premise.toHtml : Premise → Lean.MetaM ProofWidgets.Html

Print a premise using HTML.

structure Mathlib.Tactic.ClickSuggestions.State : Type

The global state that is shared between all threads.

• status : Std.HashMap String Nat

  The ongoing computations.

• progress : Bool

  Whether any progress has been made at all. If all computations have been finished and no progress has been made, then inform the user.

• solvedSuggestions : Array ProofWidgets.Html

  The suggestions that close the goal.

structure Mathlib.Tactic.ClickSuggestions.Context : Type

The information required for pasting a suggestion into the editor.

• meta : Lean.Server.DocumentMeta

  The current document

• cursorPos : Lean.Lsp.Position

  The range that should be replaced. In tactic mode, this should be the range of the suggestion tactic. In infoview mode, the start and end of the range should both be the cursor position.

• onGoal : Option Nat

  Whether to use the on_goal n => combinator.

• stx : Option (Lean.TSyntax `tactic)

  The preceding piece of syntax, if available. It is not available if the cursor is at the start of the next tactic. This is used for merging consecutive rw tactics.

• masterToken : ProofWidgets.RefreshToken

  The token for updating the main HTML body of suggestions. This is used for displaying a message that no progress has happened.

• statusToken : ProofWidgets.RefreshToken

  The token for the ⏳️ HTML that represents the state of the ongoing computations.

• solvedToken : ProofWidgets.RefreshToken

  The token for the solved goals.

• goal : Lean.MVarId

  The main goal.

• hyp? : Option Lean.FVarId

  The selected hypothesis, if any.

• pos : Lean.SubExpr.Pos

  The position of the selected subexpression.

@[reducible, inline]

abbrev Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (α : Type) : Type

The monad used in #click_suggestions.

@[instance_reducible]

instance Mathlib.Tactic.ClickSuggestions.instMonadStateOfStateClickSuggestionsM : MonadStateOf State ClickSuggestionsM

def Mathlib.Tactic.ClickSuggestions.markProgress : ClickSuggestionsM Unit

Signify that at least one suggestion has been made.

def Mathlib.Tactic.ClickSuggestions.getHypIdent? : ClickSuggestionsM (Option Lean.Ident)

Get the syntax of the variable whose type the user selected.

def Mathlib.Tactic.ClickSuggestions.getHypIdent! : ClickSuggestionsM Lean.Ident

Get the variable whose type the user selected.

def Mathlib.Tactic.ClickSuggestions.trackingComputation {α : Type} (name : String) (k : ClickSuggestionsM α) : ClickSuggestionsM α

Run a computation in such a way that we can keep track of it.

partial def Mathlib.Tactic.ClickSuggestions.isExplicitEq (t s : Lean.Expr) : Lean.MetaM Bool

Determine whether the explicit parts of two expressions are equal, and the implicit parts are definitionally equal, up to reducible_and_instances transparency. This says whether two expressions are 'morally equal', and is used for deduplicating suggestions.

inductive Mathlib.Tactic.ClickSuggestions.RwKind : Type

Information about the rewrite position. This is used to determine whether to suggest rw, rw!, nth_rw, or simp_rw.

• hasBVars : RwKind

  rw cannot rewrite here, because the subexpression contains bound variables. So, we suggest simp_rw.

• valid (motiveTypeCorrect : Bool) (occ : Option Nat) : RwKind

  If motiveTypeCorrect := true, we suggest rw! instead of rw. If occ := some n, we suggest nth_rw n instead of rw.

def Mathlib.Tactic.ClickSuggestions.mkRewrite (kind : RwKind) (symm : Bool) (e : Lean.Term) (loc : Option Lean.Ident) (grw : Bool := false) : Lean.CoreM (Lean.TSyntax `tactic)

Construct the syntax for a rewrite tactic.

partial def Mathlib.Tactic.ClickSuggestions.mergeTactics? {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (stx₁ stx₂ : Lean.TSyntax `tactic) : m (Option (Lean.TSyntax `tactic))

Try to combine the suggested tactic with the preceding tactic in the tactic sequence. In particular, we merge sequences of rw, simp_rw and grw.

def Mathlib.Tactic.ClickSuggestions.tacticPasteString (tac : Lean.TSyntax `tactic) : ClickSuggestionsM String

Given tactic syntax tac that we want to paste into the editor, return it as a string. This function respects the 100 character limit for long lines.

def Mathlib.Tactic.ClickSuggestions.mkInsertion (tac : Lean.TSyntax `tactic) : ClickSuggestionsM (Lean.Lsp.Range × String)

Given tactic syntax tac, compute the text edit that will paste it into the editor. We return the range that should be replaced, and the new text that will replace it.

def Mathlib.Tactic.ClickSuggestions.mkSuggestion (tac : Lean.TSyntax `tactic) (html : ProofWidgets.Html) (isClosing : Bool := false) : ClickSuggestionsM ProofWidgets.Html

Generate a suggestion for inserting tac, with message html. The button is [apply] if the tactic does not close the goal, and [done] if it is closing.

def Mathlib.Tactic.ClickSuggestions.addSolvedSuggestion (tac : Lean.TSyntax `tactic) : ClickSuggestionsM Unit

Add suggestion tac to the list of tactics that solve the goal.

def Mathlib.Tactic.ClickSuggestions.kabstractFindsPositions (e p : Lean.Expr) (targetPos : Lean.SubExpr.Pos) : Lean.MetaM Bool

Return whether kabstract uniquely finds pattern p in e at position targetPos.

def Mathlib.Tactic.ClickSuggestions.hasUnhelpfulMVars (newMVars : Array Lean.MVarId) (oldMVars newExpressions : Array Lean.Expr) : Lean.MetaM Bool

Determine which metavariables count as "unhelpful", given the old and new metavariables. This is used in suggestions of e.g. apply, to filter out suggestions with unhelpful metavariables.

A metavariable is unhelpful if it was freshly introduced, and is not used in the assignment of a previously appearing metavariable.