loogle-search
starsforks
How to install loogle-search?
parcadei/continuous-claude-v3/loogle-search
$npx -y skills add parcadei/Continuous-Claude-v3 --skill loogle-searchSearch Mathlib for lemmas by type signature pattern
SKILL.md
| 1 | # Loogle Search - Mathlib Type Signature Search |
| 2 | |
| 3 | Search Mathlib for lemmas by type signature pattern. |
| 4 | |
| 5 | ## When to Use |
| 6 | |
| 7 | - Finding a lemma when you know the type shape but not the name |
| 8 | - Discovering what's available for a type (e.g., all `Nontrivial ↔ _` lemmas) |
| 9 | - Type-directed proof search |
| 10 | |
| 11 | ## Commands |
| 12 | |
| 13 | ```bash |
| 14 | # Search by pattern (uses server if running, else direct) |
| 15 | loogle-search "Nontrivial _ ↔ _" |
| 16 | loogle-search "(?a → ?b) → List ?a → List ?b" |
| 17 | loogle-search "IsCyclic, center" |
| 18 | |
| 19 | # JSON output |
| 20 | loogle-search "List.map" --json |
| 21 | |
| 22 | # Start server for fast queries (keeps index in memory) |
| 23 | loogle-server & |
| 24 | ``` |
| 25 | |
| 26 | ## Query Syntax |
| 27 | |
| 28 | | Pattern | Meaning | |
| 29 | |---------|---------| |
| 30 | | `_` | Any single type | |
| 31 | | `?a`, `?b` | Type variables (same variable = same type) | |
| 32 | | `Foo, Bar` | Must mention both `Foo` and `Bar` | |
| 33 | | `Foo.bar` | Exact name match | |
| 34 | |
| 35 | ## Examples |
| 36 | |
| 37 | ```bash |
| 38 | # Find lemmas relating Nontrivial and cardinality |
| 39 | loogle-search "Nontrivial _ ↔ _ < Fintype.card _" |
| 40 | |
| 41 | # Find map-like functions |
| 42 | loogle-search "(?a → ?b) → List ?a → List ?b" |
| 43 | # → List.map, List.pmap, ... |
| 44 | |
| 45 | # Find everything about cyclic groups and center |
| 46 | loogle-search "IsCyclic, center" |
| 47 | # → commutative_of_cyclic_center_quotient, ... |
| 48 | |
| 49 | # Find Fintype.card lemmas |
| 50 | loogle-search "Fintype.card" |
| 51 | ``` |
| 52 | |
| 53 | ## Performance |
| 54 | |
| 55 | - **With server running**: ~100-200ms per query |
| 56 | - **Cold start (no server)**: ~10s per query (loads 343MB index) |
| 57 | |
| 58 | ## Setup |
| 59 | |
| 60 | Loogle must be built first: |
| 61 | ```bash |
| 62 | cd ~/tools/loogle && lake build |
| 63 | lake build LoogleMathlibCache # or use --write-index |
| 64 | ``` |
| 65 | |
| 66 | ## Integration with Proofs |
| 67 | |
| 68 | When stuck in a Lean proof: |
| 69 | 1. Identify what type shape you need |
| 70 | 2. Query Loogle to find the lemma name |
| 71 | 3. Apply the lemma in your proof |
| 72 | |
| 73 | ```lean |
| 74 | -- Goal: Nontrivial G from 1 < Fintype.card G |
| 75 | -- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _" |
| 76 | -- Found: Fintype.one_lt_card_iff_nontrivial |
| 77 | exact Fintype.one_lt_card_iff_nontrivial.mpr h |
| 78 | ``` |
People who liked this also viewed
6 picksType
- azure-aiUse for Azure AI: Search, Speech, OpenAI, Document Intelligence. Helps with search, vector/hybrid search, speech-to-text, text-to-speech, transcription, OCR. WHEN: AI Search, query search, vector searSkillsJul 2026
- just-scrapeSearch, scrape, crawl, extract structured data, and monitor web pages via the ScrapeGraph AI CLI. Use when the user asks to search the web, scrape a webpage, grab content from a URL, extract JSON fromSkillsJul 2026
- firecrawlCLI and Agent Skill for Firecrawl - Add scrape, search, and browsing capabilities to your AI agentsSkillsJul 2026
- firecrawl-searchWeb search with full page content extraction. Use this skill whenever the user asks to search the web, find articles, research a topic, look something up, find recent news, discover sources, or says "SkillsJul 2026
- firecrawl-agentAI-powered autonomous data extraction that navigates complex sites and returns structured JSON. Use this skill when the user wants structured data from websites, needs to extract pricing tiers, producSkillsJul 2026
- firecrawl-mapDiscover and list all URLs on a website, with optional search filtering. Use this skill when the user wants to find a specific page on a large site, list all URLs, see the site structure, find where sSkillsJul 2026
