lean_loogle
Search for Lean definitions and theorems via loogle using patterns like constants, lemma names, subexpressions, type shapes, and conclusions.
Instructions
Limit: 3req/30s. Search for definitions and theorems using loogle.
Query patterns:
- By constant: Real.sin # finds lemmas mentioning Real.sin
- By lemma name: "differ" # finds lemmas with "differ" in the name
- By subexpression: _ * (_ ^ _) # finds lemmas with a product and power
- Non-linear: Real.sqrt ?a * Real.sqrt ?a
- By type shape: (?a -> ?b) -> List ?a -> List ?b
- By conclusion: |- tsum _ = _ * tsum _
- By conclusion w/hyps: |- _ < _ → tsum _ < tsum _
Args:
query (str): Search query
num_results (int, optional): Max results. Defaults to 8.
Returns:
List[dict] | str: Search results or error msg
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | ||
| num_results | No |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |