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.

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.

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."

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."

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

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

The #statesearch tactic uses the current proof state for searching based on LeanStateSearch API. It can only be used as a tactic. Note that if no valid tactics are found, it will display command suggestions with search results.

example : 0 ≤ 1 := by
  #statesearch
  sorry