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 LeanSearchClient.LoogleMatch

Equations

• LeanSearchClient.instInhabitedLoogleMatch = { default := { name := default, type := default, doc? := default } }

instance LeanSearchClient.instReprLoogleMatch : Repr LeanSearchClient.LoogleMatch

Equations

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

inductive LeanSearchClient.LoogleResult : Type

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

instance LeanSearchClient.instInhabitedLoogleResult : Inhabited LeanSearchClient.LoogleResult

Equations

• LeanSearchClient.instInhabitedLoogleResult = { default := LeanSearchClient.LoogleResult.empty }

instance LeanSearchClient.instReprLoogleResult : Repr LeanSearchClient.LoogleResult

Equations

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

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

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

Equations

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

def LeanSearchClient.loogleUsage : String

Equations

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

def LeanSearchClient.turnstyle : Lean.ParserDescr

The turnstyle uesd bin #find, unicode or ascii allowed

Equations

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

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

Equations

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

def LeanSearchClient.loogle_filters : Lean.ParserDescr

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 ", "))

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.

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

• LeanSearchClient.justLoogleCmdImpl x = pure PUnit.unit

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.

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

def LeanSearchClient.just_loogle_tactic : Lean.ParserDescr

Equations

• LeanSearchClient.just_loogle_tactic = Lean.ParserDescr.node `LeanSearchClient.just_loogle_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "#loogle" false)

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

Equations

• LeanSearchClient.justLoogleTacticImpl x = Lean.logWarning ((Lean.MessageData.ofFormat ∘ Lean.format) LeanSearchClient.loogleUsage)