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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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

## Equations

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

## Instances For

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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.

## Instances For

## Equations

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