commit: 9c527f6db4e612f9ebbabefd7faff21711192308

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Tue Sep 29 15:32:55 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Tue Sep 29 15:32:55 2026 +0000
tree: d00902e321316d1f1711fcffc1f2627bb6b2566b
parent: c279397e208e7a39fd816a961e5d77e96c8fe2dc [diff]

test: use `warn.sorry false` in `grind_bitvec2`

The benchmark produces no output now, so `grind_bitvec2.lean.out.expected` is not needed.

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

2 files changed

tree: d00902e321316d1f1711fcffc1f2627bb6b2566b

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.