LeanSearchClient

LeanSearchClient provides syntax for search using the leansearch 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:

• Command syntax: #leansearch "search query" as a command.
• Term syntax: #leansearch "search query" as a term.
• Tactic syntax: #leansearch "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.

Examples

The following are examples of using the leansearch API. The search is triggered when the sentence ends with a full stop (period) or a question mark.

Query Command

For leansearch:

#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

For moogle:

#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

Query Term

For leansearch:

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

For moogle:

example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."

Query Tactic

Note that only valid tactics are displayed.

For leansearch:

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

For moogle:

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

Loogle Search

The #loogle command can also be used in all three modes. The syntax in this case is #loogle <search query> as in the following examples.

#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry