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

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

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

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

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

def LeanSearchClient.getMoogleQueryJson (s : String) (num_results : Nat := 6) : Lean.CoreM (Array Lean.Json)

def LeanSearchClient.getStateSearchQueryJson (s : String) (num_results : Nat := 6) (rev : String) : Lean.CoreM (Array Lean.Json)

structure LeanSearchClient.SearchResult : Type

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

instance LeanSearchClient.instReprSearchResult : Repr SearchResult

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

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

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

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

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

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

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

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

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

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

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

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

structure LeanSearchClient.SearchServer : Type

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

def LeanSearchClient.leanSearchServer : SearchServer

def LeanSearchClient.moogleServer : SearchServer

instance LeanSearchClient.instInhabitedSearchServer : Inhabited SearchServer

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

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

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

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

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

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

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

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

You can modify the LeanSearch URL by setting the LEANSEARCHCLIENT_LEANSEARCH_API_URL environment variable.

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

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

You can modify the Moogle URL by setting the LEANSEARCHCLIENT_MOOGLE_API_URL environment variable.

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

def LeanSearchClient.search_cmd : Lean.ParserDescr

Search either Moogle or LeanSearch from within Lean, depending on the option leansearchclient.backend. 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.

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

example := #search "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
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.

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

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

You can modify the LeanSearch URL by setting the LEANSEARCHCLIENT_LEANSEARCH_API_URL environment variable.

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

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

You can modify the Moogle URL by setting the LEANSEARCHCLIENT_MOOGLE_API_URL environment variable.

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

def LeanSearchClient.search_term : Lean.ParserDescr

Search either Moogle or LeanSearch from within Lean, depending on the option leansearchclient.backend. 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.

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

example := #search "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
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.

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

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

You can modify the LeanSearch URL by setting the LEANSEARCHCLIENT_LEANSEARCH_API_URL environment variable.

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

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

You can modify the Moogle URL by setting the LEANSEARCHCLIENT_MOOGLE_API_URL environment variable.

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

def LeanSearchClient.statesearch_search_tactic : Lean.ParserDescr

Search LeanStateSearch from within Lean. Your current main goal is sent as query. The revision to search can be set using the statesearch.revision option. The number of results can be set using the statesearch.queries option.

Hint: If you want to modify the query, you need to use the web interface.

set_option statesearch.queries 1
set_option statesearch.revision "v4.16.0"

example : 0 ≤ 1 := by
  #statesearch
  sorry

You can modify the LeanStateSearch URL by setting the LEANSEARCHCLIENT_LEANSTATESEARCH_API_URL environment variable.

def LeanSearchClient.stateSearchTacticImpl : Lean.Elab.Tactic.Tactic

def LeanSearchClient.search_tactic : Lean.ParserDescr

Search either Moogle or LeanSearch from within Lean, depending on the option leansearchclient.backend. 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.

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

example := #search "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
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.

def LeanSearchClient.searchTacticImpl : Lean.Elab.Tactic.Tactic