commit: 427680503ea931c983b40573ba8f95c82d063d71

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

Sat Oct 24 01:12:24 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Oct 24 02:00:51 2026 +0000
tree: 33bc6273d6c5e7e253d5d6f41564f0b2697f81f8
parent: 2659c6968251bb33cd6acbd4e24e17e01b4cebab [diff]

perf: use recursor-based normalization in `lia` certificates

This PR makes the kernel check `lia` certificates faster. Certificates that normalize linear expressions now use variants of `Expr.toPoly'`, `Poly.insert`, and `Poly.norm` written with recursors and `Int.beq'`, which the kernel evaluates 2-3x faster than the versions defined by structural recursion.

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

src/Init/Data/Int/Linear.lean[diff]

1 file changed

tree: 33bc6273d6c5e7e253d5d6f41564f0b2697f81f8

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.