{"id":"loogle-search","name":"loogle-search","summary":"型シグネチャパターンで補題をMathlibで検索してください","body":"# Loogle Search - Mathlib Type Signature Search\n\nSearch Mathlib for lemmas by type signature pattern.\n\n## When to Use\n\n- Finding a lemma when you know the type shape but not the name\n- Discovering what's available for a type (e.g., all `Nontrivial ↔ _` lemmas)\n- Type-directed proof search\n\n## Commands\n\n```bash\n# Search by pattern (uses server if running, else direct)\nloogle-search \"Nontrivial _ ↔ _\"\nloogle-search \"(?a → ?b) → List ?a → List ?b\"\nloogle-search \"IsCyclic, center\"\n\n# JSON output\nloogle-search \"List.map\" --json\n\n# Start server for fast queries (keeps index in memory)\nloogle-server &\n```\n\n## Query Syntax\n\n| Pattern | Meaning |\n|---------|---------|\n| `_` | Any single type |\n| `?a`, `?b` | Type variables (same variable = same type) |\n| `Foo, Bar` | Must mention both `Foo` and `Bar` |\n| `Foo.bar` | Exact name match |\n\n## Examples\n\n```bash\n# Find lemmas relating Nontrivial and cardinality\nloogle-search \"Nontrivial _ ↔ _ < Fintype.card _\"\n\n# Find map-like functions\nloogle-search \"(?a → ?b) → List ?a → List ?b\"\n# → List.map, List.pmap, ...\n\n# Find everything about cyclic groups and center\nloogle-search \"IsCyclic, center\"\n# → commutative_of_cyclic_center_quotient, ...\n\n# Find Fintype.card lemmas\nloogle-search \"Fintype.card\"\n```\n\n## Performance\n\n- **With server running**: ~100-200ms per query\n- **Cold start (no server)**: ~10s per query (loads 343MB index)\n\n## Setup\n\nLoogle must be built first:\n```bash\ncd ~/tools/loogle && lake build\nlake build LoogleMathlibCache  # or use --write-index\n```\n\n## Integration with Proofs\n\nWhen stuck in a Lean proof:\n1. Identify what type shape you need\n2. Query Loogle to find the lemma name\n3. Apply the lemma in your proof\n\n```lean\n-- Goal: Nontrivial G from 1 < Fintype.card G\n-- Query: loogle-search \"Nontrivial _ ↔ 1 < Fintype.card _\"\n-- Found: Fintype.one_lt_card_iff_nontrivial\nexact Fintype.one_lt_card_iff_nontrivial.mpr h\n```","author":"@parcadei","ownerProfile":null,"authorContacts":null,"sourceUrl":"https://github.com/parcadei/Continuous-Claude-v3/tree/main/.claude/skills/loogle-search","license":"MIT","category":null,"lang":"en","tokens":555,"stars":0,"calls30d":2,"claimed":false,"visibility":"public","origin":"crawler","version":"0.1.0","createdAt":"2026-08-22","updatedAt":"2026-08-22","files":[],"requires":{"mcp":[],"tools":[]},"safety":{"flags":[],"scannedAt":"2026-08-22","hasScripts":false,"networkEndpoints":[]}}