# 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. 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.

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.

source
def LeanSearchClient.useragent :
Lean.CoreM String
Equations

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

Instances For

source
opaque LeanSearchClient.leanSearchCache :
IO.Ref (Std.HashMap (String × Nat) (Array Lean.Json))
source
opaque LeanSearchClient.stateSearchCache :
IO.Ref (Std.HashMap (String × Nat × String) (Array Lean.Json))
source
def LeanSearchClient.getLeanSearchQueryJson (s : String) (num_results : Nat := 6) :
Lean.CoreM (Array Lean.Json)
Equations

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

Instances For

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

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

Instances For

source
structure LeanSearchClient.SearchResult :
Type

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

Instances For

source
instance LeanSearchClient.instReprSearchResult :
Repr SearchResult
Equations

- LeanSearchClient.instReprSearchResult = { reprPrec := LeanSearchClient.instReprSearchResult.repr }

source
def LeanSearchClient.instReprSearchResult.repr :
SearchResult → Nat → Std.Format
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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.

Instances For

source
structure LeanSearchClient.SearchServer :
Type

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

Instances For

source
def LeanSearchClient.leanSearchServer :
SearchServer
Equations

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

Instances For

source
instance LeanSearchClient.instInhabitedSearchServer :
Inhabited SearchServer
Equations

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

source
def LeanSearchClient.SearchServer.getCommandSuggestions (ss : 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)

Instances For

source
def LeanSearchClient.SearchServer.getTermSuggestions (ss : 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)

Instances For

source
def LeanSearchClient.SearchServer.getTacticSuggestionGroups (ss : 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.

Instances For

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

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

Instances For

source
def LeanSearchClient.SearchServer.searchCommandSuggestions (ss : 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.

Instances For

source
def LeanSearchClient.SearchServer.searchTermSuggestions (ss : 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.

Instances For

source
def LeanSearchClient.SearchServer.searchTacticSuggestions (ss : 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.

Instances For

source
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.

Equations

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

Instances For

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

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

Instances For

source
def LeanSearchClient.search_cmd :
Lean.ParserDescr

Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch). 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.

Equations

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

Instances For

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

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

Instances For

source
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.

Equations

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

Instances For

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

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

Instances For

source
def LeanSearchClient.search_term :
Lean.ParserDescr

Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch). 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.

Equations

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

Instances For

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

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

Instances For

source
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.

Equations

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

Instances For

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

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

Instances For

source
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.

Equations

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

Instances For

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

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

Instances For

source
def LeanSearchClient.search_tactic :
Lean.ParserDescr

Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch). 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.

Equations

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

Instances For

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

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

Instances For