Loogle Search

What problem does it solve?

This Skill helps users find mathematical lemmas in Mathlib by searching for their type signature patterns, which is useful when the lemma name is unknown.

Core Features & Use Cases

• Type Signature Search: Find lemmas based on the shape of their type signatures.
• Pattern Matching: Supports wildcards (_) and type variables (?a, ?b) for flexible queries.
• Use Case: When trying to prove a theorem, you might know you need a lemma that takes a list of type ?a and returns a list of type ?b, but not its name. This Skill can find List.map or similar functions.

Quick Start

Use loogle-search to find lemmas matching the pattern "(?a → ?b) → List ?a → List ?b".