LeanSearchClient

In this file, we provide syntax for search using the leansearch API and the Moogle 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. For leansearch these are:

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

The corresponding syntax for Moogle is:

• Command syntax: #moogle "search query" as a command.
• Term syntax: #moogle "search query" as a term.
• Tactic syntax: #moogle "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.useragent : Lean.CoreM String

Equations

• LeanSearchClient.useragent = do let __do_lift ← Lean.getOptions pure (Lean.Option.get __do_lift leansearchclient.useragent)

opaque LeanSearchClient.leanSearchCache : IO.Ref (Std.HashMap (String × Nat) (Array Lean.Json))

opaque LeanSearchClient.moogleCache : IO.Ref (Std.HashMap String (Array Lean.Json))

def LeanSearchClient.getLeanSearchQueryJson (s : String) (num_results : optParam Nat 6) : Lean.CoreM (Array Lean.Json)

Equations

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

def LeanSearchClient.getMoogleQueryJson (s : String) (num_results : optParam Nat 6) : Lean.CoreM (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

instance LeanSearchClient.instReprSearchResult : Repr LeanSearchClient.SearchResult

Equations

• LeanSearchClient.instReprSearchResult = { reprPrec := LeanSearchClient.reprSearchResult✝ }

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

Equations

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

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

Equations

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

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

Equations

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

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.queryLeanSearch (s : String) (num_results : Nat) : Lean.MetaM (Array LeanSearchClient.SearchResult)

Equations

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

def LeanSearchClient.queryMoogle (s : String) (num_results : Nat) : Lean.MetaM (Array LeanSearchClient.SearchResult)

Equations

• LeanSearchClient.queryMoogle s num_results = do let jsArr ← liftM (LeanSearchClient.getMoogleQueryJson s num_results) Array.filterMapM LeanSearchClient.SearchResult.ofMoogleJson? jsArr

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.

structure LeanSearchClient.SearchServer : Type

• name : String
• url : String
• cmd : String
• query : String → Nat → Lean.MetaM (Array LeanSearchClient.SearchResult)
• queryNum : Lean.CoreM Nat

def LeanSearchClient.leanSearchServer : LeanSearchClient.SearchServer

Equations

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

def LeanSearchClient.moogleServer : LeanSearchClient.SearchServer

Equations

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

instance LeanSearchClient.instInhabitedSearchServer : Inhabited LeanSearchClient.SearchServer

Equations

• LeanSearchClient.instInhabitedSearchServer = { default := LeanSearchClient.leanSearchServer }

def LeanSearchClient.SearchServer.getCommandSuggestions (ss : LeanSearchClient.SearchServer) (s : String) (num_results : Nat) : Lean.MetaM (Array Lean.Meta.Tactic.TryThis.Suggestion)

Equations

• ss.getCommandSuggestions s num_results = do let suggestions ← ss.query s num_results pure (Array.map LeanSearchClient.SearchResult.toCommandSuggestion suggestions)

def LeanSearchClient.SearchServer.getTermSuggestions (ss : LeanSearchClient.SearchServer) (s : String) (num_results : Nat) : Lean.MetaM (Array Lean.Meta.Tactic.TryThis.Suggestion)

Equations

• ss.getTermSuggestions s num_results = do let suggestions ← ss.query s num_results pure (Array.map LeanSearchClient.SearchResult.toTermSuggestion suggestions)

def LeanSearchClient.SearchServer.getTacticSuggestionGroups (ss : LeanSearchClient.SearchServer) (s : String) (num_results : Nat) : Lean.MetaM (Array (String × Array Lean.Meta.Tactic.TryThis.Suggestion))

Equations

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

def LeanSearchClient.SearchServer.incompleteSearchQuery (ss : LeanSearchClient.SearchServer) : String

Equations

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

def LeanSearchClient.SearchServer.searchCommandSuggestions (ss : LeanSearchClient.SearchServer) (stx : Lean.Syntax) (s : Lean.TSyntax `str) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def LeanSearchClient.SearchServer.searchTermSuggestions (ss : LeanSearchClient.SearchServer) (stx : Lean.Syntax) (s : Lean.TSyntax `str) : Lean.Elab.TermElabM Unit

Equations

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

def LeanSearchClient.SearchServer.searchTacticSuggestions (ss : LeanSearchClient.SearchServer) (stx : Lean.Syntax) (s : Lean.TSyntax `str) : Lean.Elab.Tactic.TacticM Unit

Equations

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

def LeanSearchClient.leansearch_search_cmd : Lean.ParserDescr

Search LeanSearch from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

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.moogle_search_cmd : Lean.ParserDescr

Search Moogle from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

Equations

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

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

Equations

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

def LeanSearchClient.leansearch_search_term : Lean.ParserDescr

Search LeanSearch from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

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.moogle_search_term : Lean.ParserDescr

Search Moogle from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

Equations

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

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

Equations

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

def LeanSearchClient.leansearch_search_tactic : Lean.ParserDescr

Search LeanSearch from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

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.

def LeanSearchClient.moogle_search_tactic : Lean.ParserDescr

Search Moogle from within Lean. Queries should be a string that ends with a . or ?. This works as a command, as a term and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

Equations

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

def LeanSearchClient.moogleTacticImpl : Lean.Elab.Tactic.Tactic

Equations

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