- Installs
- 485
- Last 24h
- —
- Trending rank
- —
- Security
- Not audited
Install
Works with every agent the skills CLI supports.
npx skills add https://github.com/parcadei/continuous-claude-v3 --skill loogle-search- 01
Install
Run the command in your project. The CLI asks which agents to install for.
- 02
Describe the task
Ask your agent for something this skill covers. It loads loogle-search automatically when relevant.
- 03
Review the result
The agent follows the SKILL.md steps, scripts and references bundled with the skill.
SKILL.md
The instructions your agent reads when the skill is triggered.
Loogle Search - Mathlib Type Signature Search
Search Mathlib for lemmas by type signature pattern.
When to Use
- Finding a lemma when you know the type shape but not the name
- Discovering what's available for a type (e.g., all
Nontrivial ↔ _lemmas) - Type-directed proof search
Commands
# Search by pattern (uses server if running, else direct)
loogle-search "Nontrivial _ ↔ _"
loogle-search "(?a → ?b) → List ?a → List ?b"
loogle-search "IsCyclic, center"
# JSON output
loogle-search "List.map" --json
# Start server for fast queries (keeps index in memory)
loogle-server &
Query Syntax
| Pattern | Meaning |
|---|---|
_ | Any single type |
?a, ?b | Type variables (same variable = same type) |
Foo, Bar | Must mention both Foo and Bar |
Foo.bar | Exact name match |
Examples
# Find lemmas relating Nontrivial and cardinality
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"
# Find map-like functions
loogle-search "(?a → ?b) → List ?a → List ?b"
# → List.map, List.pmap, ...
# Find everything about cyclic groups and center
loogle-search "IsCyclic, center"
# → commutative_of_cyclic_center_quotient, ...
# Find Fintype.card lemmas
loogle-search "Fintype.card"
Performance
- With server running: ~100-200ms per query
- Cold start (no server): ~10s per query (loads 343MB index)
Setup
Loogle must be built first:
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache # or use --write-index
Integration with Proofs
When stuck in a Lean proof:
- Identify what type shape you need
- Query Loogle to find the lemma name
- Apply the lemma in your proof
-- Goal: Nontrivial G from 1 < Fintype.card G
-- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"
-- Found: Fintype.one_lt_card_iff_nontrivial
exact Fintype.one_lt_card_iff_nontrivial.mpr h
FAQ
What does the loogle-search skill do?
Search Mathlib for lemmas by type signature pattern
How do I install loogle-search?
Run npx skills add https://github.com/parcadei/continuous-claude-v3 --skill loogle-search in your project. The skills CLI detects the agents you use and copies the skill into the right folder. For Claude Code you can also place the skill folder at ~/.claude/skills/loogle-search/ (personal) or .claude/skills/loogle-search/ (project).
Which AI agents can use loogle-search?
Any agent that supports the open Agent Skills format (a folder with a SKILL.md file), including Claude Code, Codex, Cursor, GitHub Copilot, Gemini CLI, Windsurf, Cline, OpenCode and more.
Is loogle-search safe to install?
No partner security audit is available yet. Skills can run commands and scripts, so read the SKILL.md and any bundled files before installing.
Who maintains loogle-search?
It is published by parcadei in parcadei/continuous-claude-v3. It has 485 recorded installs.
More from parcadei/continuous-claude-v3
discovery-interview
parcadei/continuous-claude-v3
Deep interview process to transform vague ideas into detailed specs. Works for technical and non-technical users.
premortem
parcadei/continuous-claude-v3
Identify failure modes before they occur using structured risk analysis
math
parcadei/continuous-claude-v3
Unified math capabilities - computation, solving, and explanation. I route to the right tool.
github-search
parcadei/continuous-claude-v3
Search GitHub code, repositories, issues, and PRs via MCP
dead-code
parcadei/continuous-claude-v3
Find unused functions and dead code in the codebase
refactor
parcadei/continuous-claude-v3
Code refactoring workflow - analyze → plan → implement → review → validate
Popular other skills
hyperframes-cli
heygen-com/hyperframes
The HyperFrames CLI by job - scaffold, check, look at frames, edit the timeline, preview, render locally or in the cloud, publish, project history - plus reading its JSON and recovering from build or render failures.
triage
mattpocock/skills
Move issues and external PRs through a state machine of triage roles, categorise, verify, grill if needed, and write agent-ready briefs.
ask-matt
mattpocock/skills
Ask which skill or flow fits your situation. A router over the skills in this repo.
to-questionnaire
mattpocock/skills
Turn a decision you can't fully answer into a questionnaire for someone else to fill in.
loop-me
mattpocock/skills
Grill me about specs for the workflows I want to build, within this workspace.