Agent skill

loogle-search

Search Mathlib for lemmas by type signature pattern

parcadei3,879★ · 1 repos on radarProfile →
claude-codeMIT
Install
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search --agent claude-code

Same command for any agent — swap --agent for codex, cursor, copilot.

Facts
Files in the skill folder: 1
SKILL.md size: 2 KB
Bundled scripts: none
Path: .claude/skills/loogle-search/SKILL.md
Open the folder on GitHub →
Where it comes from
Stars: 3,879
Language: Python
Read our review of the source →

Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.

From the SKILL.md

# 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 ```bash # 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 ```bash # 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 l

What's inside
Steps it walks through
  1. When to Use
  2. Commands
  3. Query Syntax
  4. Examples
  5. Performance
  6. Setup
  7. Integration with Proofs
Commands it runs
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 &
Find lemmas relating Nontrivial and cardinality
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"
More from Continuous-Claude-v3
All skills →
About this skill
What does the loogle-search skill do?

Search Mathlib for lemmas by type signature pattern

How do I install it?

Run `npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.

Where does this skill come from?

From parcadei/Continuous-Claude-v3, a repository with 3,879 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.

Is a popular skill a good skill?

Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.

Keep going