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

• 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.success default }

instance LeanSearchClient.instReprLoogleResult : Repr LeanSearchClient.LoogleResult

Equations

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

def LeanSearchClient.getLoogleQueryJson (s : String) (num_results : optParam 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

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.loogle_term : Lean.ParserDescr

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

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.