commit: 688ee4c88722ca191981246f7732f25caed81cac

[log]
author: Markus Himmel <markus@lean-fro.org>

Fri Nov 15 13:09:52 2024 +0100
committer: GitHub <noreply@github.com>

Fri Nov 15 12:09:52 2024 +0000
tree: 329854d14b4261570a4b60ccc934210f882ef92f
parent: 9a3dd615e0781711a7d2f9d0a9050414636149b2 [diff]

fix: constant folding for Nat.ble and Nat.blt (#6087)

This PR fixes a bug in the constant folding for the `Nat.ble` and
`Nat.blt` function in the old code generator, leading to a
miscompilation.

Closes #6086

src/Lean/Compiler/ConstFolding.lean[diff]
src/include/lean/lean.h[diff]
tests/lean/run/6086.lean[Added - diff]

3 files changed

tree: 329854d14b4261570a4b60ccc934210f882ef92f

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).