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
# 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