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.

Equations

• Mathlib.Tactic.ClickSuggestions.exprToHtml e = do let __do_lift ← Lean.Widget.ppExprTagged e pure (<ProofWidgets.InteractiveCode fmt={__do_lift}/>)

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.

Equations

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

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.

Equations

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

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.

Equations

• Mathlib.Tactic.ClickSuggestions.tacticToHtml tac = do let __do_lift ← liftM (Lean.PrettyPrinter.ppTactic tac) Mathlib.Tactic.ClickSuggestions.formatToHtmlWithDoc __do_lift tac.raw.getKind

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.

@[implicit_reducible]

instance Mathlib.Tactic.ClickSuggestions.instInhabitedPremise : Inhabited Premise

Equations

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

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

Print a premise as a string.

Equations

• (Mathlib.Tactic.ClickSuggestions.Premise.const name).toString = name.toString
• (Mathlib.Tactic.ClickSuggestions.Premise.fvar { name := name }).toString = name.toString

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

The name length of a premise.

Equations

• premise.length = premise.toString.length

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

Get the type of a premise.

Equations

• (Mathlib.Tactic.ClickSuggestions.Premise.const name).getType = (fun (x : Lean.ConstantInfo) => x.type) <$> Lean.getConstInfo name
• (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId).getType = fvarId.getType

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.

Equations

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

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

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

Equations

• (Mathlib.Tactic.ClickSuggestions.Premise.const name).unresolveName = do let __do_lift ← Lean.getOptions Lean.unresolveNameGlobalAvoidingLocals name (Lean.getPPFullNames __do_lift)
• (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId).unresolveName = fvarId.getUserName

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

Print a premise using message data.

Equations

• (Mathlib.Tactic.ClickSuggestions.Premise.const name).toMessageData = Lean.MessageData.ofConstName name
• (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId).toMessageData = Lean.MessageData.ofExpr (Lean.Expr.fvar fvarId)

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

Print a premise using HTML.

Equations

• (Mathlib.Tactic.ClickSuggestions.Premise.const name).toHtml = Mathlib.Tactic.ClickSuggestions.constToHtml name
• (Mathlib.Tactic.ClickSuggestions.Premise.fvar fvarId).toHtml = Mathlib.Tactic.ClickSuggestions.exprToHtml (Lean.Expr.fvar fvarId)

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.

Equations

• Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM = ReaderT Mathlib.Tactic.ClickSuggestions.Context (ReaderT (IO.Ref Mathlib.Tactic.ClickSuggestions.State) Lean.MetaM)

@[implicit_reducible]

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

Equations

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

def Mathlib.Tactic.ClickSuggestions.markProgress : ClickSuggestionsM Unit

Signify that at least one suggestion has been made.

Equations

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

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

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

Equations

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

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

Get the variable whose type the user selected.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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

Equations

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

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.

Equations

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