commit: 583ce45040601430c435ba94e1dc9887a1d1d2a7

[log]
author: Kim Morrison <kim@tqft.net>

Tue Dec 02 11:09:19 2025 +1100
committer: Kim Morrison <kim@tqft.net>

Tue Dec 02 11:09:19 2025 +1100
tree: bb4852a1289b07fd2874a9ccc252888f12af99fd
parent: c0d5b9b52c31c181db0902b4cc107459f9df6563 [diff]

fix: improve "no library suggestions engine registered" error message

This PR improves the error message when no library suggestions engine
is registered to recommend importing `Lean.LibrarySuggestions.Default`
for the built-in engine.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

2 files changed

tree: bb4852a1289b07fd2874a9ccc252888f12af99fd

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.