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