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.
Installation
Details
Usage
After installing, this skill will be available to your AI coding assistant.
Verify installation:
npx agent-skills-cli listSkill Instructions
name: loogle description: 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.
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"
More by takoeight0821
View allFind relevant research and guide implementation based on it. Use when implementing features, fixing bugs, or exploring techniques where existing research in docs/research/ may provide guidance. Trigger phrases include "apply research", "use research", "based on the research", "implement from paper", or "find relevant research for [task]".
Surface → IR translation rules and IR reduction semantics for Ziku's λμμ̃-calculus based intermediate representation. Use when implementing translation, IR evaluation, or understanding the core semantics.
This skill should be used when the user asks to "refactor", "extract function", "rename", "improve code quality", "reduce duplication", or "remove code smell". Supports Lean 4 and general refactoring patterns.
This skill should be used when the user asks to "create a commit", "commit changes", "write a commit message", "make a commit", needs help with "conventional commits", or wants to understand commit message format and best practices.