# 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.instInhabitedLoogleMatch = { default := { name := default, type := default, doc? := default } }

## Equations

- LeanSearchClient.instReprLoogleMatch = { reprPrec := LeanSearchClient.reprLoogleMatch✝ }

- empty: LeanSearchClient.LoogleResult
- success: Array LeanSearchClient.SearchResult → LeanSearchClient.LoogleResult
- failure: String → Option (List String) → LeanSearchClient.LoogleResult

## Instances For

## Equations

- LeanSearchClient.instReprLoogleResult = { reprPrec := LeanSearchClient.reprLoogleResult✝ }

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

The turnstyle uesd bin `#find`

, unicode or ascii allowed

## Equations

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

## Instances For

a single `#find`

filter. The `term`

can also be an ident or a strlit,
these are distinguished in `parseFindFilters`

## Equations

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

## Instances For

The argument to `#find`

, a list of filters

## Equations

- LeanSearchClient.loogle_filters = Lean.ParserDescr.nodeWithAntiquot "loogle_filters" `LeanSearchClient.loogle_filters (LeanSearchClient.loogle_filter.sepBy "," (Lean.ParserDescr.symbol ", "))

## Instances For

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

```
#loogle List ?a → ?a
example := #loogle List ?a → ?a
example : 3 ≤ 5 := by
#loogle Nat.succ_le_succ
sorry
```

## Loogle Usage #

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring: 🔍 "differ" finds all lemmas that have "differ" somewhere in their lemma name.

By subexpression: 🔍 _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map: 🔍 (?a -> ?b) -> List ?a -> List ?b 🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion: 🔍 |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, 🔍 |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search 🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

## Equations

- LeanSearchClient.loogle_cmd = Lean.ParserDescr.node `LeanSearchClient.loogle_cmd 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#loogle") LeanSearchClient.loogle_filters)

## Instances For

## Equations

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

## Instances For

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

```
#loogle List ?a → ?a
example := #loogle List ?a → ?a
example : 3 ≤ 5 := by
#loogle Nat.succ_le_succ
sorry
```

## Loogle Usage #

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring: 🔍 "differ" finds all lemmas that have "differ" somewhere in their lemma name.

By subexpression: 🔍 _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map: 🔍 (?a -> ?b) -> List ?a -> List ?b 🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion: 🔍 |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, 🔍 |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search 🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

## Equations

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

## Instances For

## Equations

## Instances For

Search Loogle from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.

```
#loogle List ?a → ?a
example := #loogle List ?a → ?a
example : 3 ≤ 5 := by
#loogle Nat.succ_le_succ
sorry
```

## Loogle Usage #

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring: 🔍 "differ" finds all lemmas that have "differ" somewhere in their lemma name.

By subexpression: 🔍 _ * (_ ^ _) finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map: 🔍 (?a -> ?b) -> List ?a -> List ?b 🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion: 🔍 |- tsum _ = _ * tsum _ finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example, 🔍 |- _ < _ → tsum _ < tsum _ will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search 🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _ woould find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

## Equations

- LeanSearchClient.loogle_term = Lean.ParserDescr.node `LeanSearchClient.loogle_term 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#loogle") LeanSearchClient.loogle_filters)

## Instances For

## Equations

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

## Instances For

```
#loogle List ?a → ?a
example := #loogle List ?a → ?a
example : 3 ≤ 5 := by
#loogle Nat.succ_le_succ
sorry
```

## Loogle Usage #

Loogle finds definitions and lemmas in various ways:

By constant: 🔍 Real.sin finds all lemmas whose statement somehow mentions the sine function.

The pattern can also be non-linear, as in 🔍 Real.sqrt ?a * Real.sqrt ?a

## 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.just_loogle_tactic = Lean.ParserDescr.node `LeanSearchClient.just_loogle_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "#loogle" false)