loogle-search

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