LeanSearchClient

In this file, we provide syntax for search using the leansearch API from within Lean. It allows you to search for Lean tactics and theorems using natural language.

We provide syntax to make a query and generate TryThis options to click or use a code action to use the results.

The queries are of three forms:

• Command syntax: #leansearch "search query" as a command.
• Term syntax: #leansearch "search query" as a term.
• Tactic syntax: #leansearch "search query" as a tactic.

In all cases results are displayed in the Lean Infoview and clicking these replaces the query text. In the cases of a query for tactics only valid tactics are displayed.

def LeanSearchClient.getQueryJson (s : String) (num_results : optParam Nat 6) : IO (Array Lean.Json)

Equations

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

structure LeanSearchClient.SearchResult : Type

• name : String
• type? : Option String
• docString? : Option String
• doc_url? : Option String
• kind? : Option String

def LeanSearchClient.queryNum : Lean.CoreM Nat

Equations

• LeanSearchClient.queryNum = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift leansearch.queries)

def LeanSearchClient.SearchResult.ofJson? (js : Lean.Json) : Option LeanSearchClient.SearchResult

Equations

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

def LeanSearchClient.SearchResult.query (s : String) (num_results : Nat) : IO (Array LeanSearchClient.SearchResult)

Equations

• LeanSearchClient.SearchResult.query s num_results = do let jsArr ← LeanSearchClient.getQueryJson s num_results pure (Array.filterMap LeanSearchClient.SearchResult.ofJson? jsArr)

def LeanSearchClient.SearchResult.toCommandSuggestion (sr : LeanSearchClient.SearchResult) : Lean.Meta.Tactic.TryThis.Suggestion

Equations

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

def LeanSearchClient.SearchResult.toTermSuggestion (sr : LeanSearchClient.SearchResult) : Lean.Meta.Tactic.TryThis.Suggestion

Equations

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

def LeanSearchClient.SearchResult.toTacticSuggestions (sr : LeanSearchClient.SearchResult) : Array Lean.Meta.Tactic.TryThis.Suggestion

Equations

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

def LeanSearchClient.getQueryCommandSuggestions (s : String) (num_results : Nat) : IO (Array Lean.Meta.Tactic.TryThis.Suggestion)

Equations

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

def LeanSearchClient.getQueryTermSuggestions (s : String) (num_results : Nat) : IO (Array Lean.Meta.Tactic.TryThis.Suggestion)

Equations

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

def LeanSearchClient.getQueryTacticSuggestionGroups (s : String) (num_results : Nat) : IO (Array (String × Array Lean.Meta.Tactic.TryThis.Suggestion))

Equations

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

def LeanSearchClient.defaultTerm (expectedType? : Option Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• LeanSearchClient.defaultTerm (some type) = if (!type.hasExprMVar) = true then Lean.Meta.mkAppM `sorryAx #[type, Lean.mkConst `Bool.false] else pure (Lean.mkConst `True.intro)
• LeanSearchClient.defaultTerm none = pure (Lean.mkConst `True.intro)

def LeanSearchClient.checkTactic (target : Lean.Expr) (tac : Lean.Syntax) : Lean.Elab.TermElabM (Option Nat)

Equations

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

def LeanSearchClient.incompleteQuery : String

Equations

• LeanSearchClient.incompleteQuery = "#leansearch query should end with a `.` or `?`.\nNote this command sends your query to an external service at https://leansearch.net/."

def LeanSearchClient.leansearch_cmd : Lean.ParserDescr

Equations

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

def LeanSearchClient.leanSearchCommandImpl : Lean.Elab.Command.CommandElab

Equations

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

def LeanSearchClient.leansearch_term : Lean.ParserDescr

Equations

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

def LeanSearchClient.leanSearchTermImpl : Lean.Elab.Term.TermElab

Equations

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

def LeanSearchClient.leansearch_tactic : Lean.ParserDescr

Equations

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

def LeanSearchClient.leanSearchTacticImpl : Lean.Elab.Tactic.Tactic

Equations

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