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.

structure LeanSearchClient.LoogleMatch : Type

• name : String
• type : String
• doc? : Option String

instance LeanSearchClient.instInhabitedLoogleMatch : Inhabited LoogleMatch

instance LeanSearchClient.instReprLoogleMatch : Repr LoogleMatch

inductive LeanSearchClient.LoogleResult : Type

• empty : LoogleResult
• success : Array SearchResult → LoogleResult
• failure (error : String) (suggestions : Option (List String)) : LoogleResult

instance LeanSearchClient.instInhabitedLoogleResult : Inhabited LoogleResult

instance LeanSearchClient.instReprLoogleResult : Repr LoogleResult

opaque LeanSearchClient.loogleCache : IO.Ref (Std.HashMap (String × Nat) LoogleResult)

def LeanSearchClient.getLoogleQueryJson (s : String) (num_results : Nat := 6) : Lean.CoreM LoogleResult

def LeanSearchClient.loogleUsage : String

def LeanSearchClient.turnstyle : Lean.ParserDescr

The turnstyle uesd bin #find, unicode or ascii allowed

def LeanSearchClient.loogle_filter : Lean.ParserDescr

a single #find filter. The term can also be an ident or a strlit, these are distinguished in parseFindFilters

def LeanSearchClient.loogle_filters : Lean.ParserDescr

The argument to #find, a list of filters

def LeanSearchClient.loogle_cmd : Lean.ParserDescr

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.

You can modify the Loogle server URL by setting the LEANSEARCHCLIENT_LOOGLE_API_URL environment variable.

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

def LeanSearchClient.just_loogle_cmd : Lean.ParserDescr

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.

You can modify the Loogle server URL by setting the LEANSEARCHCLIENT_LOOGLE_API_URL environment variable.

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

def LeanSearchClient.loogle_term : Lean.ParserDescr

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.

You can modify the Loogle server URL by setting the LEANSEARCHCLIENT_LOOGLE_API_URL environment variable.

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

def LeanSearchClient.loogle_tactic : Lean.ParserDescr

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.

You can modify the Loogle server URL by setting the LEANSEARCHCLIENT_LOOGLE_API_URL environment variable.

def LeanSearchClient.loogleTacticImpl : Lean.Elab.Tactic.Tactic

def LeanSearchClient.just_loogle_tactic : Lean.ParserDescr

def LeanSearchClient.justLoogleTacticImpl : Lean.Elab.Tactic.Tactic