ReddRadar
Agent skill
loogle
Search for Lean 4 and Mathlib theorems, lemmas, and definitions by type signature, name, or subexpression pattern. Use when the user asks to find a theorem, look up a Lean definition, search for lemmas, or needs help discovering Mathlib functions.
Install this agent skill to your Project
npx add-skill https://github.com/majiayu000/claude-skill-registry/tree/main/skills/development/loogle-takoeight0821-ziku
SKILL.md
Loogle - Lean/Mathlib Search
Search for Lean 4 and Mathlib declarations using the Loogle API.
How to Search
Use WebFetch to query the Loogle JSON API:
https://loogle.lean-lang.org/json?q=<URL-encoded-query>
Query Syntax
| Type | Syntax | Example |
|---|---|---|
| By constant | ConstantName |
List.map |
| By name substring | "text" |
"differ" |
| By subexpression | _ * (_ ^ _) |
Pattern matching |
| By type signature | (?a -> ?b) -> List ?a -> List ?b |
Type search |
| By conclusion | ` | - goal` |
| Combined | filter1, filter2 |
AND logic |
Response Handling
Success response:
count: Total matches foundhits: Array of results (max 200)name: Declaration nametype: Type signaturemodule: Source moduledoc: Documentation (may be null)
Error response:
error: Error messagesuggestions: Array of suggested corrections
When presenting results, show the declaration name, type signature, and module. Include documentation if available.
Example Queries
- Find list functions:
List, ?a -> ?b - Search by name:
"append" - Type signature:
Nat -> Nat -> Bool - Parsec functions:
Std.Internal.Parsec - Option operations:
Option, "map"
Recommended Agent Skills
Expand your agent's capabilities with these related and highly-rated skills.
majiayu000/claude-skill-registry
agent-ops-spec
Manage specification documents in .agent/specs/. Use when user provides requirements, acceptance criteria, or feature descriptions that need to be tracked and validated against implementation.
majiayu000/claude-skill-registry
agent-ops-state
Maintain .agent state files. Use at session start, after meaningful steps, and before concluding: read/update constitution/memory/focus/issues/baseline consistently.
majiayu000/claude-skill-registry
agent-ops-spec
Manage specification documents in .agent/specs/. Use when user provides requirements, acceptance criteria, or feature descriptions that need to be tracked and validated against implementation.
majiayu000/claude-skill-registry
agent-ops-testing
Test strategy, execution, and coverage analysis. Use when designing tests, running test suites, or analyzing test results beyond baseline checks.
majiayu000/claude-skill-registry
agent-ops-testing
Test strategy, execution, and coverage analysis. Use when designing tests, running test suites, or analyzing test results beyond baseline checks.
majiayu000/claude-skill-registry
agent-ops-state
Maintain .agent state files. Use at session start, after meaningful steps, and before concluding: read/update constitution/memory/focus/issues/baseline consistently.
Didn't find tool you were looking for?