commit: f893b1ea6ea95cc9045623b79cb8ad5d1b7d62d3

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

Fri Dec 12 18:18:06 2025 +0100
committer: Leonardo de Moura <leomoura@amazon.com>

Fri Dec 12 18:19:47 2025 +0100
tree: 89047fc533cb43f453018628d3854026910cc880
parent: 9df8a80c7d371efbdac4044d6f14e1c6fb5f0b28 [diff]

feat: bitvec literal internalization in `grind`

This PR fixes bitvector literal internalization in `grind`. The fix
ensures theorems indexed by `BitVec.ofNat` are properly activated.

2 files changed

tree: 89047fc533cb43f453018628d3854026910cc880

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.