commit: c88ec35c0db43ab95e70eb829a62b287031e7959

[log]
author: Henrik Böving <hargonix@gmail.com>

Fri Dec 19 19:09:32 2025 +0100
committer: GitHub <noreply@github.com>

Fri Dec 19 18:09:32 2025 +0000
tree: d0858fd4d1659cc91493f87a80d8c38b2ffddefd
parent: 73ff198d11410054def5223123a58de85f06d3dd [diff]

perf: turn more commonly used bv_decide theorems into simprocs (#11739)

This PR turns even more commonly used bv_decide theorems that require
unification into fast simprocs
using syntactic equality. This pushes the overall performance across
sage/app7 to <= 1min10s for
every problem.

4 files changed

tree: d0858fd4d1659cc91493f87a80d8c38b2ffddefd

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.