commit: 1d9639fe5faf7bb9a0e8c7a2a8c6f2286b11b638

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

Wed Jan 07 11:15:57 2026 +1100
committer: Kim Morrison <kim@tqft.net>

Wed Jan 07 12:20:32 2026 +1100
tree: 4d8353cd5101f7061de9f76b7d2c61ec7139a140
parent: 26f4572f9fc8ab78d201290ff897e4618a352cc0 [diff]

fix: use correct APIs for MessageLog.empty and String.contains

- Replace `.empty` with `MessageLog.empty` (no EmptyCollection instance)
- Replace `.containsSubstr` with `.contains` (containsSubstr doesn't exist)

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

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

2 files changed

tree: 4d8353cd5101f7061de9f76b7d2c61ec7139a140

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.