LeanSearchClient¶
LeanSearchClient 提供了在 Lean 内使用 leansearch API、Moogle API 和 LeanStateSearch API 进行搜索的语法。它允许你使用自然语言搜索 Lean 的策略和定理，同时也支持在 Lean 内对 Loogle 进行搜索。
我们提供了用于发起查询的语法，并生成 TryThis 选项，方便你点击或使用代码操作来利用搜索结果。查询共有四种形式：
Command语法：以命令形式使用#search "search query"。Term语法：以项的形式使用#search "search query"。Tactic语法：以策略形式使用#search "search query"。- 基于状态的
Tactic语法：直接使用#search。
在所有情况下，结果都会显示在 Lean 信息视图中，点击结果会替换原查询文本。而在策略查询中，只会显示有效的策略。
所使用的后端由 leansearchclient.backend 选项决定。
示例¶
以下是使用 leansearch API 的示例。当查询语句以句号或问号结束时，搜索将会被触发。
查询 command¶
适用于所有后端的通用命令：
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."
我们还为特定后端提供了命令。例如，对于 leansearch：
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
对于 moogle：
#moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
查询 Term¶
通用命令：
example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
对于 leansearch：
example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
对于 moogle：
example := #moogle "If a natural number n is less than m, then the successor of n is less than the successor of m."
查询 Tactic¶
请注意，只会显示有效的策略。
通用命令有两种变体。一种是带字符串的形式，调用 LeanSearch 或 Moogle：
example : 3 ≤ 5 := by
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."
sorry
另一种是不带字符串的形式，调用 LeanStateSearch：
example : 3 ≤ 5 := by
#search
sorry
不同后端也有各自的特定命令。
对于 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
对于 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
对于 LeanStateSearch：
example : 3 ≤ 5 := by
#statesearch
sorry
Loogle 搜索¶
#loogle 命令也可以在所有三种模式下使用。其语法为 #loogle <search query>，例如：
#loogle List ?a → ?a
example := #loogle List ?a → ?a
example : 3 ≤ 5 := by
#loogle Nat.succ_le_succ
sorry